isEquiv_iff_val_sub_one_lt_one — Mathlib

English

Let v and v′ be valuations on a field K with value groups Γ0 and Γ′0, respectively. Then v and v′ are equivalent if and only if for every x in K we have v(x − 1) < 1 exactly when v′(x − 1) < 1.

Русский

Пусть v и v′ — оценивания поля K со значениями в группах Γ0 и Γ′0. Тогда они эквивалентны тогда и только тогда, когда для каждого x ∈ K верно v(x − 1) < 1 тогда и только тогда, когда v′(x − 1) < 1.

LaTeX

$$$v \ IsEquiv \ v' \iff \forall {x \in K},\ v(x-1) < 1 \iff v'(x-1) < 1$$$

Lean4

theorem isEquiv_iff_val_sub_one_lt_one [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
    {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} : v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
  by
  rw [isEquiv_iff_val_lt_one]
  exact (Equiv.subRight 1).surjective.forall

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