English
Let p be prime, n,k,b with k ≤ n and log_p n < b. Then the p-adic exponent of C(n, k) equals the cardinality of the set {i ∈ Ico(1,b) : p^i ≤ k mod p^i + (n−k) mod p^i}.
Русский
Пусть p — простое, n,k,b с k ≤ n и log_p n < b. Тогда показатель p в C(n,k) равен кардиналу множества {i ∈ Ico(1,b): p^i ≤ k mod p^i + (n−k) mod p^i}.
LaTeX
$$$ (\\mathrm{choose}(n,k)).factorization p = \\#\\{ i ∈ \\mathrm{Ico}(1,b) \\mid p^i ≤ k \\bmod p^i + (n-k) \\bmod p^i \\}. $$$
Lean4
/-- The factorization of `p` in `choose n k` is the number of carries when `k` and `n - k`
are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
is any bound greater than `log p n`. -/
theorem factorization_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb : log p n < b) :
(choose n k).factorization p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) := by
rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]
