English
For prime p and natural numbers k ≤ n, the p-adic exponent in C(n, k) is determined by a decomposition expressing the carry structure when adding k and n−k in base p.
Русский
Для простого p и целых k ≤ n разложение факторизации p в C(n,k) задаётся разложением, отражающим переносы при сложении k и n−k в основание p.
LaTeX
$$$ (n \\choose k).factorization p = \\#\\{ i ∈ Ico(1,b) \\mid p^i ≤ k \\bmod p^i + (n-k) \\bmod p^i \\}. $$$
Lean4
theorem multiplicity_choose_aux {p n b k : ℕ} (hp : p.Prime) (hkn : k ≤ n) :
∑ i ∈ Finset.Ico 1 b, n / p ^ i =
((∑ i ∈ Finset.Ico 1 b, k / p ^ i) + ∑ i ∈ Finset.Ico 1 b, (n - k) / p ^ i) +
#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) :=
calc
∑ i ∈ Finset.Ico 1 b, n / p ^ i = ∑ i ∈ Finset.Ico 1 b, (k + (n - k)) / p ^ i := by
simp only [add_tsub_cancel_of_le hkn]
_ = ∑ i ∈ Finset.Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) := by
simp only [Nat.add_div (pow_pos hp.pos _)]
_ = _ := by simp [sum_add_distrib, sum_boole]
