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