one — Mathlib

English

The trivial valuation sends every nonzero element to 1 and 0 to 0.

Русский

Тривиальная оценка отправляет каждый ненулевой элемент в 1, а 0 в 0.

LaTeX

$$$(1 : Valuation\\ R\\ Γ_0)\\ x = \\begin{cases}0 & x=0 \\\\ 1 & x \\neq 0\\end{cases}$$$

Lean4

/-- The trivial valuation, sending everything to 1 other than 0. -/
protected instance one : One (Valuation R Γ₀) where
  one :=
    { __ : R →*₀ Γ₀ := 1
      map_add_le_max' x
        y :=
        by
        simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe, MonoidWithZeroHom.one_apply_def, le_sup_iff]
        split_ifs <;> simp_all }

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