Jordan–Hölder for groups

Stream: maths

[Brendan Seamas Murphy]

I formalized a proof of Jordan–Hölder a while back and just got around to closing the last admit. Is there any interest in adding this to mathlib? I don't know the conventions for merging code, and it's fairly sloppy right now, so I would probably need help on making it fit the style guide (I assume mathlib has one of those?). It's up at https://github.com/Shamrock-Frost/jordan-holder

[Johan Commelin]

Cool! Sure, feel free to PR this. There might be lots of comments and feedback. But together we can certainly get it into mathlib shape.