English
Let p be prime. Then (p·(n+1))! has p-adic exponent equal to the sum of the p-adic exponents of (p·n)! and (n+1)! plus 1.
Русский
Пусть p — простое. Тогда v_p((p(n+1))!) = v_p((pn)!) + v_p((n+1)!) + 1.
LaTeX
$$$ (p \\cdot (n+1))!.factorization p = (p \\cdot n)!.factorization p + (n+1).factorization p + 1. $$$
Lean4
/-- A logarithmic upper bound on the multiplicity of a prime in a binomial coefficient. -/
theorem factorization_choose_le_log : (choose n k).factorization p ≤ log p n :=
by
by_cases h : (choose n k).factorization p = 0
· simp [h]
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h
have hkn : k ≤ n := by
refine le_of_not_gt fun hnk => h ?_
simp [choose_eq_zero_of_lt hnk]
rw [factorization_choose hp hkn (Nat.lt_add_one _)]
exact (card_filter_le ..).trans_eq (Nat.card_Ico _ _)
