padicValNat_le_nat_log — Mathlib

English

For any p and n, the p-adic valuation of n does not exceed the p-logarithm of n.

Русский

Для любых p и n p-адическая оценка n не превосходит логарифма по основанию p от n.

LaTeX

$$$\\forall p,n \\in \\mathbb{N},\\ \\operatorname{padicValNat}(p,n) \\le \\log p\\, n$$$

Lean4

/-- The p-adic valuation of `n` is less than or equal to its logarithm w.r.t. `p`. -/
theorem padicValNat_le_nat_log (n : ℕ) : padicValNat p n ≤ Nat.log p n :=
  by
  rcases n with _ | n
  · simp
  rcases p with _ | _ | p
  · simp
  · simp
  exact Nat.le_log_of_pow_le p.one_lt_succ_succ (le_of_dvd n.succ_pos pow_padicValNat_dvd)

Похожие утверждения