Center_of_Group_of_Order_Prime_Cubed_v2
Provedcentergroup-theoryp-groupproofwiki
If G is a group of order p^3 where p is prime, then |Z(G)| ≠ p^2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Center_of_Group_of_Order_Prime_Cubed_v2 {G : Type _} [Group G] [Fintype G] [DecidableEq G] {p : ℕ} (hp : Nat.Prime p) (hG : Fintype.card G = p ^ 3) : Nat.card (Subgroup.center G) ≠ p ^ 2 := by sorrySource