English
For prime p, and n ≠ 0, log_p n equals padicValNat p n if and only if n < p^{padicValNat p n + 1}.
Русский
Пусть p — простое, n ≠ 0. Тогда log_p n = v_p(n) тогда и только тогда, когда n < p^{v_p(n)+1}.
LaTeX
$$$\\forall p,n \\ (hp:\\text{Fact}(\\text{Nat.Prime}(p))) \\ (hn:\\, n \\neq 0) \\Rightarrow \\operatorname{log} p n = \\operatorname{padicValNat} p n \\iff n < p^{\\operatorname{padicValNat} p n + 1}$$$
Lean4
/-- **Legendre's Theorem**
Taking (`p - 1`) times the `p`-adic valuation of `n!` equals `n` minus the sum of base `p` digits
of `n`. -/
theorem sub_one_mul_padicValNat_factorial [hp : Fact p.Prime] (n : ℕ) :
(p - 1) * padicValNat p (n !) = n - (p.digits n).sum :=
by
rw [padicValNat_factorial <| lt_succ_of_lt <| lt.base (log p n)]
nth_rw 2 [← zero_add 1]
rw [Nat.succ_eq_add_one, ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.succ_eq_add_one]
