Theorems · Definition · order theory

CompositionSeries.Equivalent

{X : Type u} → [inst : Lattice X] → [inst_1 : JordanHolderLattice X] → CompositionSeries X → CompositionSeries X → Prop

Two CompositionSeries X, s₁ and s₂ are equivalent if there is a bijection e : Fin s₁.length ≃ Fin s₂.length such that for any i, Iso (s₁ i) (s₁ i.succ) (s₂ (e i), s₂ (e i.succ))

Defined in

Mathlib.Order.JordanHolder

Cited by

9 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

LatticeJordanHolderLattice