groups of order p²

Stream: Is there code for X?

[Jakub Kądziołka]

Do we have anything stating that there are only two isomorphism classes of order p² groups (where p is prime)? If not, I think I'd like to formalize that...

[Alex J. Best]

I dont know that we have that, we have docs#is_p_group.center_nontrivial though which should be useful

[Riccardo Brasca]

Knowing that the center is non trivial makes things very easy: the quotient over the center has order 1 or p, so it's always cyclic , hence the group is abelian (do we have this?) and from here it shouldn't be hard.

[Alex J. Best]

@Jakub Kądziołka did you end up working on this, the triage bot just reminded me of #8632

[Jakub Kądziołka]

huh, other stuff came up, but thanks for the link, it'll certainly come in useful once I get to this