norm_eq_zpow_neg_valuation — Mathlib

English

For any nonzero PadicSeq f, its norm equals p to the power of the negative of its valuation, i.e., f.norm = (p)^{ - valuation(f) }.

Русский

Для любой ненулевой PadicSeq f нормa равна p в степени минус оценки f, то есть f.norm = p^{ - valuation(f) }.

LaTeX

$$$f.norm = p^{ -\mathrm{valuation}(f) }$$$

Lean4

theorem norm_eq_zpow_neg_valuation {f : PadicSeq p} (hf : ¬f ≈ 0) : f.norm = (p : ℚ) ^ (-f.valuation : ℤ) :=
  by
  rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg]
  intro H
  apply CauSeq.not_limZero_of_not_congr_zero hf
  intro ε hε
  use stationaryPoint hf
  intro n hn
  rw [stationaryPoint_spec hf le_rfl hn]
  simpa [H] using hε

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