Theorems · Inductive type · order theory

JordanHolderLattice

(X : Type u) → [Lattice X] → Type u

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

Cited by

44 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Lattice