zero_iff — Mathlib

English

For a valuation on a division ring with nontrivial Γ₀, v(x) = 0 iff x = 0.

Русский

Для валюации на делительном кольце с ненулевой Γ₀ верно: v(x) = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$ v(x) = 0 \iff x = 0 $$$

Lean4

/-- If `v` is a valuation on a division ring then `v(x) = 0` iff `x = 0`. -/
theorem zero_iff [Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K} : v x = 0 ↔ x = 0 :=
  map_eq_zero v

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