Group_of_Order_Prime_Squared_is_Abelian
Provedabeliangroup-theoryp-groupprime-powerproofwiki
A group whose order is the square of a prime is abelian.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Group_of_Order_Prime_Squared_is_Abelian {G : Type _} [Group G] [Fintype G] {p : ℕ} (hp : Nat.Prime p) (hG : Fintype.card G = p ^ 2) (a b : G) : a * b = b * a := by sorrySource