valuation_ofNat — Mathlib

English

For n ∈ ℕ, the valuation of the p-adic number corresponding to n equals padicValNat p n (via ofNat).

Русский

Для n ∈ ℕ, нормa p-адического числа, соответствующего n, равна padicValNat p n.

LaTeX

$$$\\mathrm{valuation}(\\operatorname{ofNat}(n): \\mathbb{Q}_p) = \\mathrm{padicValNat}(p,n)$$$

Lean4

@[simp]
theorem valuation_ofNat (n : ℕ) [n.AtLeastTwo] : valuation (ofNat(n) : ℚ_[p]) = padicValNat p n :=
  valuation_natCast n

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