English
For any prime p, max(log_p n, v_p(n+1)) equals log_p(n+1).
Русский
Для любого простого p максимум из log_p n и v_p(n+1) равен log_p(n+1).
LaTeX
$$$\\forall p,n \\ (p\\text{ prime}) \\Rightarrow \\max(\\log p n,\\operatorname{padicValNat} p (n+1)) = \\log p (n+1)$$$
Lean4
/-- **Kummer's Theorem**
The `p`-adic valuation of `(n + k).choose k` is the number of carries when `k` and `n` are added
in base `p`. This sum is expressed over the finset `Ico 1 b` where `b` is any bound greater than
`log p (n + k)`. -/
theorem padicValNat_choose' {n k b : ℕ} [hp : Fact p.Prime] (hnb : log p (n + k) < b) :
padicValNat p (choose (n + k) k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) := by
exact_mod_cast
(padicValNat_eq_emultiplicity (p := p) <| choose_ne_zero <| Nat.le_add_left k n) ▸
Prime.emultiplicity_choose' hp.out hnb
