Theorems · Definition · commutative algebra

Valuation.IsEquiv.orderMonoidIso

{R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : LinearOrderedCommGroupWithZero Γ₀] →
        [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] →
          [inst_2 : Ring R] →
            {v : Valuation R Γ₀} →
              {w : Valuation R Γ'₀} →
                v.IsEquiv w → (MonoidWithZeroHom.ofClass v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass w).ValueGroup₀

The isomorphism between the ValueGroup₀'s of two equivalent valuations.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroRing