Theorems · Theorem · order theory

CompositionSeries.Equivalent.trans

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ s₃ : CompositionSeries X},
  s₁.Equivalent s₂ → s₂.Equivalent s₃ → s₁.Equivalent s₃

Defined in

Mathlib.Order.JordanHolder

Cited by

2 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice