Commit 2024-05-30 11:03 d09a6fc8

refactor(Order/JordanHolder): use RelSeries to implement CompositionSeries (#12914)

[!NOTE] The TODO in this file indicates that the instance of JordanHolderLattice for submodules should be obtained via ModularLattice. This is not the case in mathlib4. See JordanHolderModule.instJordanHolderLattice.