English
For every natural number n, the natural logarithm of n equals the sum over primes p of the exponent t_p in the prime factorization of n times log p. In particular, log n = ∑_{p prime} v_p(n) log p, where n = ∏ p^{v_p(n)}; the case n = 0 is handled separately and trivial.
Русский
Для любого натурального числа n справедливо log n = ∑_{p \\\\text{ -простые}} v_p(n) log p, где n = ∏ p^{v_p(n)}; случай n = 0 обрабатывается отдельно.
LaTeX
$$$$ \\log n = \\sum_{p \\text{ prime}} v_p(n) \\log p \\quad (n = \\prod_{p} p^{v_p(n)}). $$$$
Lean4
theorem log_nat_eq_sum_factorization (n : ℕ) : log n = n.factorization.sum fun p t => t * log p :=
by
rcases eq_or_ne n 0 with (rfl | hn)
·
simp -- relies on junk values of `log` and `Nat.factorization`
· simp only [← log_pow, ← Nat.cast_pow]
rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.factorization_prod_pow_eq_self hn]
intro p hp
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
