Theorems · Theorem · commutative algebra

Valuation.IsEquiv.trans

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [inst : Ring R]
  [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀]
  [inst_3 : LinearOrderedCommMonoidWithZero Γ''₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {v₃ : Valuation R Γ''₀},
  v₁.IsEquiv v₂ → v₂.IsEquiv v₃ → v₁.IsEquiv v₃

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

3 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext

Assumes

RingLinearOrderedCommMonoidWithZeroLinearOrderedCommMonoidWithZeroLinearOrderedCommMonoidWithZero