Binomial_Coefficient_of_Prime
Provedbinomial-coefficientsprime-numbersproofwiki
If p is prime and 0 < k < p, then p divides C(p,k).
Preamble
import Mathlib.Data.Nat.Choose.Factorization
Formal statement
theorem Binomial_Coefficient_of_Prime (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk0 : 0 < k) (hkp : k < p) : p ∣ Nat.choose p k := by sorry
Source