Composition Series for Groups wrt Normal subgroup

Stream: Is there code for X?

[Johannes Choo]

I found the analogous theory for modules, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/SimpleModule/Basic.html .

It is an instance of an abstraction in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/JordanHolder.html

so I'd like to contribute a parallel development for groups in this file if it's indeed missing https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Subgroup/Simple.html

Note: previous discussion that I could find #maths > Jordan Hölder theorem

[Johan Commelin]

@Thomas Browning probably knows best...

[Johannes Choo]

TODO

Provide instances of [JordanHolderLattice](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/JordanHolder.html#JordanHolderLattice) for subgroups, and potentially for modular lattices.

I improved my reading comprehension and am a bit more convinced it doesn't exist yet XD

[Thomas Browning]

@Chris Hughes was the one working on this, but I suspect that you're right and we don't have Jordan-Holder for subgroups yet.

[Chris Hughes]

My memory of this is that the proof of Jordan-Holder currently in the library should apply to groups as long as you can prove they form a JordanHolderLattice, but I have a feeling that there is a little bit of content to this and it won't be as easy as for modules.