English
Let p be a prime and a a nonnegative integer. Then for all n,k, 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 ∈ ℕ. Тогда 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=0}^{a-1} \\binom{(n / p^i) \\bmod p}{(k / p^i) \\bmod p} \\pmod p. $$$
Lean4
/-- For primes `p`, `choose n k` is congruent to the product of `choose (⌊n / p ^ i⌋ % p)
(⌊k / p ^ i⌋ % p)` over i < a, multiplied by `choose (⌊n / p ^ a⌋) (⌊k / p ^ a⌋)`, modulo `p`. -/
theorem choose_modEq_choose_mul_prod_range_choose (a : ℕ) :
choose n k ≡ choose (n / p ^ a) (k / p ^ a) * ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p] :=
match a with
| Nat.zero => by simp
| Nat.succ a =>
(choose_modEq_choose_mul_prod_range_choose a).trans <|
by
rw [prod_range_succ, cast_mul, ← mul_assoc, mul_right_comm]
gcongr
apply choose_modEq_choose_mod_mul_choose_div.trans
simp_rw [pow_succ, Nat.div_div_eq_div_mul, mul_comm, Int.ModEq.refl]
