Structures · Order
JordanHolderLattice
A JordanHolderLattice is the class for which the Jordan Hölder theorem is proved. A
Jordan Hölder lattice is a lattice equipped with a notion of maximality, IsMaximal.
Examples include Subgroup G if G is a group, and Submodule R M if M is an R-module.
In the example of subgroups, IsMaximal H K means that H is a maximal normal subgroup of K.
In the example of submodules, IsMaximal M N means that M is a maximal submodule of N.
- Defined in
- Mathlib.Order.JordanHolder
- Shape
- One type argument · adds IsMaximal, lt_of_isMaximal, sup_eq_of_isMaximal, isMaximal_inf_left_of_isMaximal_sup
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by45
- JordanHolderLattice.IsMaximal
- CompositionSeries
- JordanHolderLattice.Iso
- CompositionSeries.Equivalent
- CompositionSeries.strictMono
- JordanHolderLattice.iso_refl
- JordanHolderLattice.lt_of_isMaximal
- CompositionSeries.isMaximal_eraseLast_last
- CompositionSeries.eq_snoc_eraseLast
- JordanHolderLattice.iso_symm
- CompositionSeries.Equivalent.trans
- CompositionSeries.mem_eraseLast
- CompositionSeries.Equivalent.snoc
- CompositionSeries.length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero
- CompositionSeries.injective
- CompositionSeries.toList_sorted
- CompositionSeries.le_last_of_mem
- JordanHolderLattice.sup_eq_of_isMaximal
- CompositionSeries.le_last
- CompositionSeries.eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero
- JordanHolderLattice.isMaximal_inf_left_of_isMaximal_sup
- JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup
- CompositionSeries.snoc_eraseLast_last
- JordanHolderLattice.second_iso
- CompositionSeries.Equivalent.snoc_snoc_swap
- CompositionSeries.Equivalent.refl
- JordanHolderLattice.second_iso_of_eq
- CompositionSeries.lt_succ
- CompositionSeries.mem_eraseLast_of_ne_of_mem
- JordanHolderLattice.iso_trans
- CompositionSeries.length_pos_of_head_eq_head_of_last_eq_last_of_length_pos
- JordanHolderLattice.isMaximal_of_eq_inf
- CompositionSeries.exists_last_eq_snoc_equivalent
- CompositionSeries.head_le
- CompositionSeries.head_le_of_mem
- CompositionSeries.jordan_holder
- CompositionSeries.toList_nodup
- CompositionSeries.total
- CompositionSeries.Equivalent.smash
- CompositionSeries.Equivalent.symm
- JordanHolderLattice.Iso.rel
- CompositionSeries.lt_last_of_mem_eraseLast
- CompositionSeries.last_eraseLast_le
- CompositionSeries.Equivalent.length_eq
- JordanHolderLattice.IsMaximal.iso_refl
Ancestors0
No ancestors.