trivialRel_eq_ofValuation_one — Mathlib

English

Under a trivial relation, the group of units of ValueGroupWithZero R is a singleton.

Русский

При тривиальном отношении множество единиц ValueGroupWithZero R единично.

LaTeX

$$$\\text{Subsingleton}((\\mathrm{ValueGroupWithZero} R)^{\\times})$$$

Lean4

theorem trivialRel_eq_ofValuation_one : trivialRel = ValuativeRel.ofValuation (1 : Valuation R Γ) :=
  by
  convert (eq_trivialRel_of_compatible_one (Γ := Γ)).symm
  exact Valuation.Compatible.ofValuation 1

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