Center_of_Group_of_Prime_Power_Order_is_Non_Trivial
Provedcentergroup-theoryp-groupprime-powerproofwiki
If G is a group of prime power order p^r (r > 0), then the center Z(G) is non-trivial.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Center_of_Group_of_Prime_Power_Order_is_Non_Trivial {G : Type _} [Group G] [Fintype G] {p : ℕ} (hp : Nat.Prime p) {r : ℕ} (hr : 0 < r) (hG : Fintype.card G = p ^ r) : Subgroup.center G ≠ ⊥ := by sorrySource