English
For a prime p, the p-adic valuation of n! equals the sum of floor(n/p^i) over i from 1 up to bound b with log p n < b (i.e., ν_p(n!) = ∑_{i∈Ico(1,b)} ⌊n/p^i⌋).
Русский
Для простого p p-адическая кратность n! равна сумме floor(n/p^i) по i от 1 до некого b > log_p n.
LaTeX
$$$ \nu_p(n!) = \sum_{i \in Ico(1,b)} \left\lfloor \dfrac{n}{p^i} \right\rfloor, \ \text{где } b > \log_p n $$$
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 emultiplicity_factorial {p : ℕ} (hp : p.Prime) :
∀ {n b : ℕ}, log p n < b → emultiplicity p n ! = (∑ i ∈ Ico 1 b, n / p ^ i : ℕ)
| 0, b, _ => by simp [Ico, hp.emultiplicity_one]
| n + 1, b, hb =>
calc
emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1) := by
rw [factorial_succ, hp.emultiplicity_mul, add_comm]
_ = (∑ i ∈ Ico 1 b, n / p ^ i : ℕ) + #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) := by
rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
_ = (∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0) : ℕ) :=
by
rw [sum_add_distrib, sum_boole]
simp
_ = (∑ i ∈ Ico 1 b, (n + 1) / p ^ i : ℕ) := congr_arg _ <| Finset.sum_congr rfl fun _ _ => Nat.succ_div.symm
