English
For a prime p and any n,b with log_p n < b, the exponent of p in n! equals the sum over i in Ico(1,b) of floor(n / p^i).
Русский
Пусть p — простое, и для любых n,b с log_p n < b верно: показатель p в n! равен сумме по i в Ico(1,b) от floor(n / p^i).
LaTeX
$$$ (n)!.factorization\\ p = \\sum_{i \\in \\mathrm{Ico}(1,b)} \\frac{n}{p^i} \quad (\\text{при } \\log_p n < b). $$$
Lean4
/-- **Legendre's Theorem**
The multiplicity of a prime in `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 factorization_factorial {p : ℕ} (hp : p.Prime) :
∀ {n b : ℕ}, log p n < b → (n)!.factorization p = ∑ i ∈ Ico 1 b, n / p ^ i
| 0, b, _ => by simp
| n + 1, b, hb =>
calc
(n + 1)!.factorization p = (n + 1).factorization p + (n)!.factorization p := by
rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero, coe_add, Pi.add_apply]
_ = #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i :=
by
rw [factorization_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), add_left_inj]
apply factorization_eq_card_pow_dvd_of_lt hp (zero_lt_succ n) (lt_pow_of_log_lt hp.one_lt hb)
_ = ∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0) := by
simp [Nat.add_comm, sum_add_distrib, sum_boole]
_ = ∑ i ∈ Ico 1 b, (n + 1) / p ^ i := Finset.sum_congr rfl fun _ _ => Nat.succ_div.symm
