Topic: Jordan–Hölder for groups
Brendan Seamas Murphy (Dec 13 2019 at 00:52):
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 (Dec 13 2019 at 06:01):
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.
Last updated: May 12 2021 at 08:14 UTC