Binomial_Coefficient_of_Prime_Plus_One_Modulo_Prime
Provedcombinatoricsnumber-theoryproofwiki
For a prime p and 2 <= k <= p-1, C(p+1, k) is congruent to 0 modulo p.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Binomial_Coefficient_of_Prime_Plus_One_Modulo_Prime (p k : ℕ) (hp : Nat.Prime p) (hk2 : 2 ≤ k) (hkp : k ≤ p - 1) : (Nat.choose (p + 1) k) % p = 0 := by sorry
Source