norm_eq_zpow_neg_valuation — Mathlib

English

For x ∈ ℚ_p, x ≠ 0, ‖x‖_p = p^{−x.valuation}.

Русский

Для x ∈ ℚ_p, x ≠ 0, ‖x‖_p = p^{−x.valuation}.

LaTeX

$$$x \\ne 0 \\Rightarrow \\|x\\|_p = p^{-\\operatorname{valuation}(x)}$$$

Lean4

theorem norm_eq_zpow_neg_valuation {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = (p : ℝ) ^ (-x.valuation) :=
  by
  refine Quotient.inductionOn' x fun f hf => ?_
  change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)
  rw [PadicSeq.norm_eq_zpow_neg_valuation]
  · rw [Rat.cast_zpow, Rat.cast_natCast]
  · apply CauSeq.not_limZero_of_not_congr_zero
    contrapose! hf
    apply Quotient.sound
    simpa using hf

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