JordanHolder

📁 Source: Mathlib/Order/JordanHolder.lean

Statistics

Metric	Count
Definitions `CompositionSeries`, `Equivalent`, `JordanHolderLattice`, `IsMaximal`	4
Theorems `length_eq`, `refl`, `smash`, `snoc`, `snoc_snoc_swap`, `trans`, `eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero`, `eq_snoc_eraseLast`, `exists_last_eq_snoc_equivalent`, `ext`, `ext_iff`, `head_le`, `head_le_of_mem`, `inj`, `injective`, `isMaximal_eraseLast_last`, `jordan_holder`, `last_eraseLast_le`, `le_last`, `le_last_of_mem`, `length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero`, `length_pos_of_head_eq_head_of_last_eq_last_of_length_pos`, `lt_last_of_mem_eraseLast`, `lt_succ`, `mem_eraseLast`, `mem_eraseLast_of_ne_of_mem`, `snoc_eraseLast_last`, `strictMono`, `toList_nodup`, `toList_sorted`, `total`, `iso_refl`, `isMaximal_inf_left_of_isMaximal_sup`, `isMaximal_inf_right_of_isMaximal_sup`, `isMaximal_of_eq_inf`, `iso_symm`, `iso_trans`, `lt_of_isMaximal`, `second_iso`, `second_iso_of_eq`, `sup_eq_of_isMaximal`	41
Total	45

CompositionSeries

Definitions

Name	Category	Theorems
`Equivalent` 📖	MathDef	8 math math: `jordan_holder`, `Equivalent.trans`, `Equivalent.snoc_snoc_swap`, `exists_last_eq_snoc_equivalent`, `Equivalent.snoc`, `Equivalent.symm`, `Equivalent.smash`, `Equivalent.refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero` 📖	—	`RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.last` `RelSeries.length`	—	—	`RelSeries.subsingleton_of_length_eq_zero` `RelSeries.last_mem` `length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero` `ext`
`eq_snoc_eraseLast` 📖	mathematical	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	`RelSeries.snoc` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.eraseLast` `RelSeries.last` `isMaximal_eraseLast_last`	—	`ext` `isMaximal_eraseLast_last` `mem_eraseLast` `RelSeries.last_mem`
`exists_last_eq_snoc_equivalent` 📖	mathematical	`JordanHolderLattice.IsMaximal` `RelSeries.last` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.head`	`CompositionSeries` `RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.length` `RelSeries.last` `Equivalent` `RelSeries.snoc`	—	`ne_of_gt` `lt_of_le_of_lt` `JordanHolderLattice.lt_of_isMaximal` `RelSeries.subsingleton_of_length_eq_zero` `RelSeries.last_mem` `RelSeries.head_mem` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `snoc_eraseLast_last` `JordanHolderLattice.isMaximal_of_eq_inf` `isMaximal_eraseLast_last` `le_inf` `le_last_of_mem` `inf_comm` `RelSeries.head_snoc` `RelSeries.last_snoc` `eq_snoc_eraseLast` `Equivalent.snoc` `JordanHolderLattice.IsMaximal.iso_refl` `Equivalent.trans` `Equivalent.snoc_snoc_swap` `JordanHolderLattice.iso_symm` `JordanHolderLattice.second_iso_of_eq` `JordanHolderLattice.sup_eq_of_isMaximal`
`ext` 📖	—	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	—	—	`RelSeries.toList_injective` `List.Perm.eq_of_pairwise'` `instAntisymmLt` `List.SortedLT.pairwise` `toList_sorted` `List.perm_of_nodup_nodup_toFinset_eq` `toList_nodup`
`ext_iff` 📖	mathematical	—	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	—	`ext`
`head_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.toFun`	—	`StrictMono.monotone` `strictMono`
`head_le_of_mem` 📖	mathematical	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal`	—	`Set.mem_range` `head_le`
`inj` 📖	mathematical	—	`RelSeries.toFun` `setOf` `JordanHolderLattice.IsMaximal`	—	`injective`
`injective` 📖	mathematical	—	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.toFun`	—	`StrictMono.injective` `strictMono`
`isMaximal_eraseLast_last` 📖	mathematical	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	`JordanHolderLattice.IsMaximal` `RelSeries.last` `setOf` `RelSeries.eraseLast`	—	`RelSeries.last_eraseLast` `RelSeries.last.eq_1` `RelSeries.step` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub`
`jordan_holder` 📖	mathematical	`RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.last`	`Equivalent`	—	`eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero` `Equivalent.refl` `length_pos_of_head_eq_head_of_last_eq_last_of_length_pos` `isMaximal_eraseLast_last` `exists_last_eq_snoc_equivalent` `head_le_of_mem` `RelSeries.last_mem` `RelSeries.head_eraseLast` `Equivalent.trans` `eq_snoc_eraseLast` `RelSeries.snoc.congr_simp` `Equivalent.snoc` `JordanHolderLattice.IsMaximal.iso_refl`
`last_eraseLast_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.last` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.eraseLast`	—	`StrictMono.le_iff_le` `strictMono` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`le_last` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.toFun` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.last`	—	`StrictMono.monotone` `strictMono`
`le_last_of_mem` 📖	mathematical	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.last` `setOf` `JordanHolderLattice.IsMaximal`	—	`Set.mem_range` `le_last`
`length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero` 📖	mathematical	`RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.last` `RelSeries.length`	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	—	`injective` `zero_add`
`length_pos_of_head_eq_head_of_last_eq_last_of_length_pos` 📖	mathematical	`RelSeries.head` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.last` `RelSeries.length`	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	—	`not_imp_not` `Nat.instCanonicallyOrderedAdd` `length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero`
`lt_last_of_mem_eraseLast` 📖	mathematical	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries` `RelSeries.membership` `RelSeries.eraseLast`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.last` `setOf` `JordanHolderLattice.IsMaximal`	—	`lt_of_le_of_ne` `le_last_of_mem` `mem_eraseLast`
`lt_succ` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.toFun` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.length`	—	`JordanHolderLattice.lt_of_isMaximal` `RelSeries.step`
`mem_eraseLast` 📖	mathematical	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	`RelSeries` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.membership` `RelSeries.eraseLast` `CompositionSeries`	—	`ne_of_lt` `mem_eraseLast_of_ne_of_mem`
`mem_eraseLast_of_ne_of_mem` 📖	mathematical	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	`RelSeries` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.membership` `RelSeries.eraseLast`	—	`RelSeries.length_pos_of_nontrivial` `RelSeries.last_mem` `lt_of_le_of_ne`
`snoc_eraseLast_last` 📖	mathematical	`JordanHolderLattice.IsMaximal` `RelSeries.last` `setOf` `RelSeries.eraseLast`	`RelSeries.snoc` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.eraseLast` `RelSeries.last`	—	`ne_of_gt` `JordanHolderLattice.lt_of_isMaximal` `Nat.instCanonicallyOrderedAdd` `zero_add` `isMaximal_eraseLast_last` `eq_snoc_eraseLast`
`strictMono` 📖	mathematical	—	`StrictMono` `RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal` `PartialOrder.toPreorder` `Fin.instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.toFun`	—	`Fin.strictMono_iff_lt_succ` `lt_succ`
`toList_nodup` 📖	mathematical	—	`RelSeries.toList` `setOf` `JordanHolderLattice.IsMaximal`	—	`List.SortedLT.nodup` `toList_sorted`
`toList_sorted` 📖	mathematical	—	`List.SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `RelSeries.toList` `setOf` `JordanHolderLattice.IsMaximal`	—	`List.IsChain.sortedLT` `RelSeries.toList_getElem` `strictMono`
`total` 📖	mathematical	`CompositionSeries` `RelSeries.membership` `setOf` `JordanHolderLattice.IsMaximal`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`Set.mem_range` `StrictMono.le_iff_le` `strictMono` `le_total`

CompositionSeries.Equivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_eq` 📖	mathematical	`CompositionSeries.Equivalent`	`RelSeries.length` `setOf` `JordanHolderLattice.IsMaximal`	—	`Fintype.card_fin` `Fintype.card_congr`
`refl` 📖	mathematical	—	`CompositionSeries.Equivalent`	—	`JordanHolderLattice.IsMaximal.iso_refl` `RelSeries.step`
`smash` 📖	mathematical	`RelSeries.last` `setOf` `JordanHolderLattice.IsMaximal` `RelSeries.head` `CompositionSeries.Equivalent`	`CompositionSeries.Equivalent` `RelSeries.smash` `setOf` `JordanHolderLattice.IsMaximal`	—	`RelSeries.smash_castAdd` `RelSeries.smash_succ_castAdd` `finSumFinEquiv_symm_apply_castAdd` `RelSeries.smash_natAdd` `RelSeries.smash_succ_natAdd` `finSumFinEquiv_symm_apply_natAdd`
`snoc` 📖	mathematical	`JordanHolderLattice.IsMaximal` `RelSeries.last` `setOf` `CompositionSeries.Equivalent` `JordanHolderLattice.Iso`	`CompositionSeries.Equivalent` `RelSeries.snoc` `setOf` `JordanHolderLattice.IsMaximal`	—	`RelSeries.snoc_castSucc` `RelSeries.last_snoc'` `finSuccEquivLast_last` `finSuccEquivLast_symm_none` `finSuccEquivLast_castSucc` `finSuccEquivLast_symm_some`
`snoc_snoc_swap` 📖	mathematical	`JordanHolderLattice.IsMaximal` `RelSeries.last` `setOf` `RelSeries.snoc` `JordanHolderLattice.Iso`	`CompositionSeries.Equivalent` `RelSeries.snoc` `setOf` `JordanHolderLattice.IsMaximal`	—	`Equiv.swap_apply_left` `RelSeries.snoc_castSucc` `RelSeries.last_snoc` `Equiv.swap_apply_right` `RelSeries.last_snoc'` `Equiv.swap_apply_of_ne_of_ne` `JordanHolderLattice.IsMaximal.iso_refl` `RelSeries.step`
`trans` 📖	mathematical	`CompositionSeries.Equivalent`	`CompositionSeries.Equivalent`	—	`JordanHolderLattice.iso_trans`

JordanHolderLattice

Definitions

Name	Category	Theorems
`IsMaximal` 📖	MathDef	31 math math: `Module.length_compositionSeries`, `CompositionSeries.le_last`, `CompositionSeries.last_eraseLast_le`, `isFiniteLength_iff_exists_compositionSeries`, `CompositionSeries.lt_last_of_mem_eraseLast`, `isMaximal_of_eq_inf`, `CompositionSeries.lt_succ`, `CompositionSeries.Equivalent.snoc_snoc_swap`, `exists_compositionSeries_of_isNoetherian_isArtinian`, `isMaximal_inf_left_of_isMaximal_sup`, `CompositionSeries.exists_last_eq_snoc_equivalent`, `CompositionSeries.Equivalent.snoc`, `CompositionSeries.Equivalent.length_eq`, `CompositionSeries.strictMono`, `CompositionSeries.head_le_of_mem`, `CompositionSeries.ext_iff`, `CompositionSeries.injective`, `CompositionSeries.snoc_eraseLast_last`, `isMaximal_inf_right_of_isMaximal_sup`, `CompositionSeries.mem_eraseLast`, `CompositionSeries.toList_sorted`, `CompositionSeries.mem_eraseLast_of_ne_of_mem`, `CompositionSeries.eq_snoc_eraseLast`, `CompositionSeries.length_pos_of_head_eq_head_of_last_eq_last_of_length_pos`, `CompositionSeries.Equivalent.smash`, `CompositionSeries.toList_nodup`, `CompositionSeries.isMaximal_eraseLast_last`, `CompositionSeries.le_last_of_mem`, `CompositionSeries.inj`, `CompositionSeries.head_le`, `CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal_inf_left_of_isMaximal_sup` 📖	mathematical	`IsMaximal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`IsMaximal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`isMaximal_inf_right_of_isMaximal_sup` 📖	mathematical	`IsMaximal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`IsMaximal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`inf_comm` `isMaximal_inf_left_of_isMaximal_sup` `sup_comm`
`isMaximal_of_eq_inf` 📖	mathematical	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `IsMaximal`	`IsMaximal`	—	`sup_eq_of_isMaximal` `isMaximal_inf_right_of_isMaximal_sup`
`iso_symm` 📖	mathematical	`Iso`	`Iso`	—	—
`iso_trans` 📖	mathematical	`Iso`	`Iso`	—	—
`lt_of_isMaximal` 📖	mathematical	`IsMaximal`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`second_iso` 📖	mathematical	`IsMaximal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Iso` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`second_iso_of_eq` 📖	mathematical	`IsMaximal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`Iso`	—	`second_iso`
`sup_eq_of_isMaximal` 📖	mathematical	`IsMaximal`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—

JordanHolderLattice.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_refl` 📖	mathematical	`JordanHolderLattice.IsMaximal`	`JordanHolderLattice.Iso`	—	`JordanHolderLattice.second_iso_of_eq` `sup_eq_right` `le_of_lt` `JordanHolderLattice.lt_of_isMaximal` `inf_eq_left`

(root)

Definitions

Name	Category	Theorems
`CompositionSeries` 📖	CompOp	5 math math: `isFiniteLength_iff_exists_compositionSeries`, `exists_compositionSeries_of_isNoetherian_isArtinian`, `CompositionSeries.exists_last_eq_snoc_equivalent`, `CompositionSeries.ext_iff`, `CompositionSeries.mem_eraseLast`
`JordanHolderLattice` 📖	CompData	—

---

← Back to Index