isEquiv_iff_valuationSubring — Mathlib

English

Two valuations are equivalent iff their valuation subrings are equal.

Русский

Две оценки эквивалентны тогда, когда их valuationSubring совпадает.

LaTeX

$$v1.IsEquiv v2 \iff v1.valuationSubring = v2.valuationSubring$$

Lean4

theorem isEquiv_iff_valuationSubring : v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring :=
  by
  constructor
  · intro h; ext x; specialize h x 1; simpa using h
  · intro h; apply isEquiv_of_val_le_one
    intro x
    have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]
    simpa using this

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