one_apply_eq_zero_iff — Mathlib

English

In a nontrivial value group, the unit valuation evaluates x to zero exactly when x is zero: (1) x = 0 iff x = 0.

Русский

В ненулевой группе значений единичная валюация даёт нулевое значение точно тогда, когда x равно нулю.

LaTeX

$$$ (1 : \\mathrm{Valuation}(R,\\Gamma_0))\\;x = 0 \\Longleftrightarrow x = 0 $$$

Lean4

@[simp]
theorem one_apply_eq_zero_iff [Nontrivial Γ₀] {x : R} : (1 : Valuation R Γ₀) x = 0 ↔ x = 0 :=
  MonoidWithZeroHom.one_apply_eq_zero_iff

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