PR #15464: feat(group_theory): Groups of order p^2 are ab...

Stream: triage

[Random Issue Bot]

Today I chose PR 15464 for discussion!

feat(group_theory): Groups of order p^2 are abelian
Created by @Sidharth Hariharan (@thefundamentaltheor3m) on 2022-07-17
Labels:

Is this PR still relevant? Any recent updates? Anyone making progress?

[Thomas Browning]

This is in mathlib now: docs#is_p_group.comm_group_of_card_eq_prime_sq

[Yaël Dillies]

Should we close this, then?

[Kevin Buzzard]

Yes let's close it, we don't need it twice. This was a student project and it's served its purpose.