English
For nonzero n, log_2 n is not equal to v_2(n+1).
Русский
Для ненулевого n логарифм по основанию 2 числа n не равен v_2(n+1).
LaTeX
$$$\\forall n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow \\log_2 n \\neq \\operatorname{padicValNat}(2, n+1)$$$
Lean4
/-- **Kummer's Theorem**
The `p`-adic valuation of `n.choose k` is the number of carries when `k` and `n - k` 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`. -/
theorem padicValNat_choose {n k b : ℕ} [hp : Fact p.Prime] (hkn : k ≤ n) (hnb : log p n < b) :
padicValNat p (choose n k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}) := by
exact_mod_cast
(padicValNat_eq_emultiplicity (p := p) <| (choose_ne_zero hkn)) ▸ Prime.emultiplicity_choose hp.out hkn hnb
