ValueGroup — Mathlib

English

The value group of the valuation associated to A is a linear ordered commutative group with zero.

Русский

Группа значений оценки, связанная с A, является линейно упорядоченной коммутативной группой с элементом ноль.

LaTeX

$$$ValueGroup(A,K) \text{ is a LinearOrderedCommGroupWithZero}$$$

Lean4

/-- The value group of the valuation associated to `A`. Note: it is actually a group with zero. -/
def ValueGroup :=
  ValuationRing.ValueGroup A K
deriving LinearOrderedCommGroupWithZero

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