English
Let p be a prime. For any a ∈ ℕ, if n < p^a and k < p^a, then C(n,k) ≡ C(n / p^a, k / p^a) · ∏_{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) ≡ C(n / p^a, k / p^a) · ∏_{i=0}^{a-1} C((n / p^i) mod p, (k / p^i) mod p) (mod p).
LaTeX
$$$ \\binom{n}{k} \\equiv \\binom{n / p^a}{k / p^a} \\cdot \\prod_{i \\in \\text{range}(a)} \\binom{(n / p^i) \\bmod p}{(k / p^i) \\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_nat {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
choose n k ≡ ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [MOD p] :=
by
rw [← Int.natCast_modEq_iff]
exact_mod_cast choose_modEq_prod_range_choose ha₁ ha₂
