Theorems · Theorem · commutative algebra

Valuation.IsEquiv.orderMonoidIso_trans

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : LinearOrderedCommGroupWithZero Γ''₀] [inst_3 : Ring R]
  {v : Valuation R Γ₀} {w : Valuation R Γ'₀} {u : Valuation R Γ''₀} (h : v.IsEquiv w) (h' : w.IsEquiv u),
  h.orderMonoidIso.trans h'.orderMonoidIso = ⋯.orderMonoidIso

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroRing