English
Let p be a prime. For any a ∈ ℕ, we have
Русский
Пусть p — простое. Для любого a ∈ ℕ имеем
LaTeX
$$$ \\forall {n k p} [p\\text{ prime}],\\; C(n,k) \\equiv C\\left( \\left\\lfloor \\frac{n}{p^a} \\right\\rfloor, \\left\\lfloor \\frac{k}{p^a} \\right\\rfloor \\right) \\cdot \\prod_{i=0}^{a-1} C\\left(\\left\\lfloor \\frac{n}{p^i} \\right\\rfloor \\bmod p, \\left\\lfloor \\frac{k}{p^i} \\right\\rfloor \\bmod p\\right) \\pmod p. $$$
Lean4
theorem choose_mul_right {m n : ℕ} (hn : n ≠ 0) : (m * n).choose n = m * (m * n - 1).choose (n - 1) :=
by
by_cases hm : m = 0
· simp only [hm, zero_mul, choose_eq_zero_iff]
exact Nat.pos_of_ne_zero hn
· set p := m - 1; have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
simp only [hp]
rw [add_mul, one_mul, choose_mul_add hn]
