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=0}^{a-1} \\binom{(n / p^i) \\bmod p}{(k / p^i) \\bmod p} \\pmod p. $$$
Lean4
theorem choose_mul_add {m n : ℕ} (hn : n ≠ 0) : (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1) :=
by
rw [← Nat.mul_left_inj (mul_ne_zero (factorial_ne_zero (m * n)) (factorial_ne_zero n))]
set p := n - 1
have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm
simp only [hp, add_succ_sub_one]
calc
(m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
(m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! :=
by ring
_ = (m * (p + 1) + (p + 1))! := by rw [add_choose_mul_factorial_mul_factorial]
_ = ((m * (p + 1) + p) + 1)! := by ring_nf
_ = ((m * (p + 1) + p) + 1) * (m * (p + 1) + p)! := by rw [factorial_succ]
_ = (m * (p + 1) + p)! * ((p + 1) * (m + 1)) := by ring
_ = ((m * (p + 1) + p).choose p * (m * (p + 1))! * (p)!) * ((p + 1) * (m + 1)) := by
rw [add_choose_mul_factorial_mul_factorial]
_ = (m * (p + 1) + p).choose p * (m * (p + 1))! * (((p + 1) * (p)!) * (m + 1)) := by ring
_ = (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1)) := by rw [factorial_succ]
_ = (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!) := by ring
