Theorems · Theorem · order theory

CompositionSeries.Equivalent.snoc

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X}
  {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s₁) x₁}
  {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s₂) x₂},
  s₁.Equivalent s₂ →
    JordanHolderLattice.Iso (RelSeries.last s₁, x₁) (RelSeries.last s₂, x₂) →
      CompositionSeries.Equivalent (RelSeries.snoc s₁ x₁ hsat₁) (RelSeries.snoc s₂ x₂ hsat₂)

Defined in

Mathlib.Order.JordanHolder

Cited by

2 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice