English
The p-adic valuation of n! equals the sum of floor(n/p^i) over i.
Русский
p-адическая оценка n! равна сумме floor(n/p^i) по i (Лежандерова формула).
LaTeX
$$$\\forall p,n,b\\ (hp:\\text{Prime}(p)\\ ),\\ v_p(n!) = \\sum_{i\\in \\mathrm{Ico}\\,1\\,b} \\left\\lfloor \\frac{n}{p^i} \\right\\rfloor$$$
Lean4
/-- **Legendre's Theorem**
The `p`-adic valuation of `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed
over the finset `Ico 1 b` where `b` is any bound greater than `log p n`. -/
theorem padicValNat_factorial {n b : ℕ} [hp : Fact p.Prime] (hnb : log p n < b) :
padicValNat p (n !) = ∑ i ∈ Finset.Ico 1 b, n / p ^ i := by
exact_mod_cast
((padicValNat_eq_emultiplicity (p := p) <| factorial_ne_zero _) ▸ Prime.emultiplicity_factorial hp.out hnb)
