exists_lt_one — Mathlib

English

For field K and valuation v, v.IsNontrivial iff there exists x with x ≠ 0 and v(x) < 1.

Русский

Для поля K и валюации v: не тривиальность эквивалентна существованию x ≠ 0 с v(x) < 1.

LaTeX

$$$ v.IsNontrivial \\iff \\exists x, x \\neq 0 \\land v x < 1 $$$

Lean4

theorem exists_lt_one {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation K Γ₀} [hv : v.IsNontrivial] :
    ∃ x : K, v x ≠ 0 ∧ v x < 1 :=
  by
  obtain ⟨x, hx⟩ := isNontrivial_iff_exists_unit.mp hv
  rw [ne_iff_lt_or_gt] at hx
  rcases hx with hx | hx
  · use x
    simp [hx]
  · use x⁻¹
    simp [-map_inv₀, ← one_lt_val_iff, hx]

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