Theorems · Definition · commutative algebra

ValuativeRel.ValueGroupWithZero.orderMonoidIso

{R : Type u_2} →
  {Γ : Type u_3} →
    [inst : Ring R] →
      [inst_1 : ValuativeRel R] →
        [inst_2 : LinearOrderedCommGroupWithZero Γ] →
          (v : Valuation R Γ) →
            [v.Compatible] → ValuativeRel.ValueGroupWithZero R ≃*o (MonoidWithZeroHom.ofClass v).ValueGroup₀

If a valuation v is compatible with the valuative relation, then ValueGroupWithZero R is isomorphic to the image group (with zero) of v as an ordered group with zero.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

13 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroValuation.Compatible