ValueGroup — Mathlib

English

The value group of the valuation ring A is defined as the quotient of the orbit relation by Aˣ acting on K.

Русский

Группа значений оценивания кольца A определяется как фактор-применение орбитальной эквивалентности элемента Aˣ на K.

LaTeX

$$$\mathrm{ValueGroup}(A,K) := \operatorname{Quotient} (\mathrm{MulAction.orbitRel} (A^{\times}) K)$$$

Lean4

/-- The value group of the valuation ring `A`. Note: this is actually a group with zero. -/
def ValueGroup : Type v :=
  Quotient (MulAction.orbitRel Aˣ K)

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