isNontrivial_iff_exists_unit — Mathlib

English

A nontrivial valuation on a field K has a unit with valuation not equal to 1.

Русский

Не тривиальная валюация на поле K имеет единицу с значением отличным от 1.

LaTeX

$$$ \\exists x : K^{\\times}, v x \\neq 1 $$$

Lean4

/-- For fields, being nontrivial is equivalent to the existence of a unit with valuation
not equal to `1`. -/
theorem isNontrivial_iff_exists_unit : w.IsNontrivial ↔ ∃ x : Kˣ, w x ≠ 1 :=
  ⟨fun ⟨x, hx0, hx1⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩
    ⟨Units.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩,
    fun ⟨x, hx⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩
    ⟨x, w.ne_zero_iff.mpr (Units.ne_zero x), hx⟩⟩

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