English
Let p be a prime number and k, n be natural numbers with k ≠ 0 and k ≠ p^n. Then p divides the binomial coefficient (p^n choose k).
Русский
Пусть p — простое число и k, n ∈ ℕ такие, что k ≠ 0 и k ≠ p^n. Тогда p делит биномиальный коэффициент C(p^n, k).
LaTeX
$$$\operatorname{Prime}(p) \land k \neq 0 \land k \neq p^n \Rightarrow p \mid \binom{p^n}{k}$$$
Lean4
theorem dvd_choose_pow (hp : Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ (p ^ n).choose k :=
by
obtain hkp | hkp := hkp.symm.lt_or_gt
· simp [choose_eq_zero_of_lt hkp]
refine emultiplicity_ne_zero.1 fun h => hkp.not_ge <| Nat.le_of_dvd hk.bot_lt ?_
have H := hp.emultiplicity_choose_prime_pow_add_emultiplicity hkp.le hk
rw [h, zero_add, emultiplicity_eq_coe] at H
exact H.1
