English
Let p be a prime and a a natural number. If n < p^a and k < p^a, then C(n,k) ≡ ∏_{i=0}^{a-1} C((n/p^i) mod p, (k/p^i) mod p) (mod p).
Русский
Пусть p — простое, a ∈ ℕ. Если n < p^a и k < p^a, то C(n,k) ≡ ∏_{i=0}^{a-1} C((n/p^i) mod p, (k/p^i) mod p) (mod p).
LaTeX
$$$ \\binom{n}{k} \\equiv \\prod_{i \\in \\text{range}(a)} \\binom{\\left(n / p^i\\right) \\bmod p}{\\left(k / p^i\\right) \\bmod p} \\pmod p. $$$
Lean4
/-- **Lucas's Theorem**: For primes `p`, `choose n k` is congruent to the product of
`choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p)` over `i` modulo `p`. -/
theorem choose_modEq_prod_range_choose {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
choose n k ≡ ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p] :=
by
apply (choose_modEq_choose_mul_prod_range_choose a).trans
simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod, Int.ModEq.refl]
