English
If G is a finite nontrivial p-group, then the center of G is nontrivial.
Русский
Если G конечная не тривиальная p-группа, то центр G не тривиален.
LaTeX
$$$\IsPGroup(p,G) \rightarrow [Nontrivial G] [Finite G] \rightarrow Nontrivial (Subgroup.center G)$$$
Lean4
theorem center_nontrivial [Nontrivial G] [Finite G] : Nontrivial (Subgroup.center G) := by
classical
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
rw [ConjAct.fixedPoints_eq_center] at this
have dvd : p ∣ Nat.card G :=
by
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
