Theorems · Theorem · order theory

CompositionSeries.jordan_holder

• 1000+ list: Jordan–Hölder theorem

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s₁ s₂ : CompositionSeries X),
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → s₁.Equivalent s₂

The Jordan-Hölder theorem, stated for any JordanHolderLattice. If two composition series start and finish at the same place, they are equivalent.

Defined in

Mathlib.Order.JordanHolder

Cited by

1 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice