English
For n ≠ 0, the p-adic valuation equals the p-logarithm precisely when n is less than p raised to one plus the valuation.
Русский
Для n ≠ 0 равенство между p-адической оценкой и p-логарифмом происходит точно тогда, когда n < p^{v_p(n)+1}.
LaTeX
$$$\\forall n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow \\operatorname{log} p n = \\operatorname{padicValNat} p n \\iff n < p^{\\operatorname{padicValNat} p n + 1}$$$
Lean4
/-- The p-adic valuation of `n` is equal to the logarithm w.r.t. `p` iff
`n` is less than `p` raised to one plus the p-adic valuation of `n`. -/
theorem nat_log_eq_padicValNat_iff {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) :
Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1) :=
by
rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by cutsat⟩), and_iff_right_iff_imp]
exact fun _ => Nat.le_of_dvd (Nat.pos_iff_ne_zero.mpr hn) pow_padicValNat_dvd
