Lucas_Theorem
Provedcombinatoricsnumber-theoryproofwiki
For prime p: C(n,k) mod p = product of C(n_i, k_i) mod p, where n_i, k_i are base-p digits.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Lucas_Theorem (p : ℕ) (hp : Nat.Prime p) (n k : ℕ) : Nat.choose n k % p = (Nat.choose (n / p) (k / p) * Nat.choose (n % p) (k % p)) % p := by sorry
Source