top_iff — Mathlib

English

If Γ0 is nontrivial, then v(x) = ⊤ iff x = 0 for x in the division ring.

Русский

Пусть Γ0 ненулево, тогда для любой x из поля, v(x) = ⊤ тогда и только тогда, когда x = 0.

LaTeX

$$$$ v(x) = \top \iff x = 0, \quad \text{assuming } [\text{Nontrivial } \Gamma_0]. $$$$

Lean4

/-- If `v` is an additive valuation on a division ring then `v(x) = ⊤` iff `x = 0`. -/
@[simp]
theorem top_iff [Nontrivial Γ₀] (v : AddValuation K Γ₀) {x : K} : v x = (⊤ : Γ₀) ↔ x = 0 :=
  v.zero_iff

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