Theorems · Definition · order theory

CompositionSeries

(X : Type u) → [inst : Lattice X] → [JordanHolderLattice X] → Type u

A CompositionSeries X is a finite nonempty series of elements of a JordanHolderLattice such that each element is maximal inside the next. The length of a CompositionSeries X is one less than the number of elements in the series. Note that there is no stipulation that a series start from the bottom of the lattice and finish at the top. For a composition series s, s.last is the largest element of the series, and s.head is the least element.

Defined in

Mathlib.Order.JordanHolder

Cited by

40 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

LatticeJordanHolderLattice