isEquiv_of_val_le_one — Mathlib

English

Alternate form: if v maps under a strictly monotone homomorphism, equivalence is preserved.

Русский

Альтернативная формулировка: если v отображается строго монотонно, эквивалентность сохраняется.

LaTeX

$$$ (\text{StrictMono } f) \rightarrow (Valuation.map f) \IsEquiv (Valuation.map f) $$$

Lean4

theorem isEquiv_of_val_le_one [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
    {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} (h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1) : v.IsEquiv v' :=
  by
  intro x y
  obtain rfl | hy := eq_or_ne y 0
  · simp
  · rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀] <;> rwa [zero_lt_iff, ne_zero_iff]

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