Binomial_Coefficient_involving_Prime
Provedcombinatoricsnumber-theoryproofwiki
Let p be a prime number. Then C(n,p) is congruent to floor(n/p) modulo p.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Binomial_Coefficient_involving_Prime (p n : ℕ) (hp : Nat.Prime p) : (Nat.choose n p) % p = (n / p) % p := by sorry
Source