not_isNontrivial_one — Mathlib

English

For a nontrivial valuation on a field K, there exists x with v(x) ≠ 0 and v(x) < 1.

Русский

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

LaTeX

$$$ \\exists x : K, v x \\neq 0 \\land v x < 1 $$$

Lean4

theorem not_isNontrivial_one [IsDomain R] [DecidablePred fun x : R ↦ x = 0] : ¬(1 : Valuation R Γ₀).IsNontrivial :=
  by
  rintro ⟨⟨x, hx, hx'⟩⟩
  rcases eq_or_ne x 0 with rfl | hx0 <;> simp_all [one_apply_of_ne_zero]

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