Zulip Chat Archive

Stream: maths

Topic: Jordan–Hölder for groups

view this post on Zulip 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

view this post on Zulip 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