Classification of small groups

Stream: Is there code for X?

[AlumKal]

Is there an exhaustive list for all groups of order at most 15?

[Jeremy Tan]

check Wikipedia? They have a list of small groups

[AlumKal]

I mean are they proved in Lean

[Mario Carneiro]

no, I think even the representation of finite groups is dicey

[Kevin Buzzard]

Do we even have a definition of Q8? Off the top of my head this will be the only group in that list which isn't a product of cyclic and dihedral groups (which we do have)

[Michael Rothgang]

I believe a student of @Floris van Doorn was working on a project to formalise this (for groups of order <= 8, or so). I don't know how far they got (but usually, student projects would need to be polished before being mathlib-ready).

[Floris van Doorn]

https://github.com/lucia3125/LeanCourse23/blob/master/LeanCourse/Project/project.lean#L706 is a classification of groups of order 8.

[Floris van Doorn]

Kevin Buzzard said:

Do we even have a definition of Q8? Off the top of my head this will be the only group in that list which isn't a product of cyclic and dihedral groups (which we do have)

Yes, it's docs#QuaternionGroup.

[Thomas Browning]

docs#isZGroup_iff_exists_mulEquiv gives a classification of groups of squarefree order, so that probably just leaves groups of order 12.