Commit 2026-07-14 16:30 aae61ae0

refactor(Order/JordanHolder): remove Iso from JordanHolderLattice (#41445) Currently JordanHolderLattice requires a choice of Iso. Different choices of Iso will lead to different strength versions of the Jordan-Holder theorem. For example, picking Iso to be "quotients have the same cardinality" will prove that any two composition series can be rearranged so that corresponding quotients have the same cardinality. But there is actually a strongest possible choice for Iso, namely the equivalence relation generated by the relations Iso (x, x ⊔ y) (x ⊓ y, y) for IsMaximal x (x ⊔ y). These are exactly the moves that are strung together to prove the Jordan-Holder theorem. Fixing Iso to be this strongest possible choice leads to the strongest possible Jordan-Holder theorem. This allows us to remove Iso from definition of JordanHolderLattice. The proof obligation IsMaximal x (x ⊔ y) → (x, x ⊔ y) ~ (x ⊓ y, y) moves from a field of JordanHolderLattice to something that the user must later prove to deduce that Iso implies the desired equivalence relation (usually "quotients are isomorphic"). This also allows us to add an instance stating that every modular lattice is a Jordan-Holder lattice, resolving a longstanding todo in the file. So we can also remove the instance stating that submodules form a Jordan-Holder lattice.