English
For prime p, and nonnegative n,k with b > log_p(n+k), the p-adic exponent of C(n+k, k) equals the number of i in Ico(1,b) with p^i ≤ k mod p^i + n mod p^i.
Русский
Для простого p, и неотрицательных n,k с b > log_p(n+k), показатель p в C(n+k,k) равен числу i в Ico(1,b) таких, что p^i ≤ k mod p^i + n mod p^i.
LaTeX
$$$ (n+k \\choose k).factorization p = \\#\\{ i ∈ Ico(1,b) \\mid p^i ≤ k % p^i + n % p^i \\}. $$$
Lean4
/-- The factorization of `p` in `choose (n + k) k` is the number of carries when `k` and `n` are
added in base `p`. The set is expressed by filtering `Ico 1 b` where `b` is any bound greater
than `log p (n + k)`. -/
theorem factorization_choose' {p n k b : ℕ} (hp : p.Prime) (hnb : log p (n + k) < b) :
(choose (n + k) k).factorization p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) :=
by
have h₁ :
(choose (n + k) k).factorization p + (k ! * n !).factorization p =
#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k ! * n !).factorization p :=
by
have h2 := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos (le_add_left k n)) (by positivity), ←
mul_assoc, h2, factorization_factorial hp hnb, factorization_mul (factorial_ne_zero k) (factorial_ne_zero n),
coe_add, Pi.add_apply, factorization_factorial hp ((log_mono_right (le_add_left k n)).trans_lt hnb),
factorization_factorial hp ((log_mono_right (le_add_left n k)).trans_lt (add_comm n k ▸ hnb)),
multiplicity_choose_aux hp (le_add_left k n)]
simp only [add_tsub_cancel_right, add_comm]
exact Nat.add_right_cancel h₁
