val_eq_iff_norm_eq — Mathlib

English

For nonzero PadicSeq f,g, f.valuation = g.valuation if and only if f.norm = g.norm.

Русский

Для ненулевых PadicSeq f,g: оценка f равна оценке g тогда и только тогда, когда нормы совпадают.

LaTeX

$$$f.valuation = g.valuation \iff f.norm = g.norm$$$

Lean4

theorem val_eq_iff_norm_eq {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) :
    f.valuation = g.valuation ↔ f.norm = g.norm :=
  by
  rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]
  · exact mod_cast (Fact.out : p.Prime).pos
  · exact mod_cast (Fact.out : p.Prime).ne_one

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