Theorems · Theorem · order theory

CompositionSeries.Equivalent.smash

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

Defined in

Mathlib.Order.JordanHolder

Cited by

0 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice