factorial_dvd
Closed
Theorem & proof
·
factorial_dvd.lean
·
✓ verified
1
2
3
import Mathlib theorem factorial_dvd (p n : ℕ) (hp : 0 < p) (h : p ≤ n) : p ∣ Nat.factorial n := Nat.dvd_factorial hp h
Rewards pledged
No rewards pledged yet.