English
For primes p, and n, k with k ≤ n, and bound b > log_p n, ν_p( n choose k ) equals the cardinality of a certain set of carries in base p.
Русский
Для простого p, и n,k с k ≤ n и b > log_p n: ν_p( n choose k ) равно кардинальности множества переносов в основание p.
LaTeX
$$$ emultiplicity(p, n \choose k) = #\{ i \in Ico(1,b) \mid p^i \le k % p^i + (n - k) % p^i \} $$$
Lean4
/-- The multiplicity 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 emultiplicity_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb : log p n < b) :
emultiplicity p (choose n k) = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) :=
by
have := Nat.sub_add_cancel hkn
convert @emultiplicity_choose' p (n - k) k b hp _
· rw [this]
exact this.symm ▸ hnb
