theorem ClassEquation.isPGroup_iff_card {G : Type u_1} [Group G] (p : ℕ) [Fact (Nat.Prime p)] [Finite G] : IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G = p ^ n

theorem ClassEquation.group_of_order_p_sq_abelian {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (hG : Nat.card G = p ^ 2) (a b : G) : a * b = b * a