English
If G is a finite p-group with order |G| = p^n and n > 0, then the center Z(G) has order p^k for some k > 0.
Русский
Если G конечна и является p-группой, и |G| = p^n с n > 0, то центр Z(G) имеет порядок p^k для некоторого k > 0.
LaTeX
$$$\exists k>0\,\, |Z(G)| = p^k.$$$
Lean4
/-- The cardinality of the `center` of a `p`-group is `p ^ k` where `k` is positive. -/
theorem card_center_eq_prime_pow (hGpn : Nat.card G = p ^ n) (hn : 0 < n) : ∃ k > 0, Nat.card (center G) = p ^ k :=
by
have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))
have hcG := to_subgroup (of_card hGpn) (center G)
rcases iff_card.1 hcG with _
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))
