Theorems · Theorem · order theory

CompositionSeries.snoc_eraseLast_last

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X}
  (h : JordanHolderLattice.IsMaximal (RelSeries.eraseLast s).last (RelSeries.last s)),
  (RelSeries.eraseLast s).snoc (RelSeries.last s) h = s

Defined in

Mathlib.Order.JordanHolder

Cited by

1 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice