English
If G is finite, G is a Z-group, and G is nontrivial, then the commutator subgroup is a proper subgroup of G.
Русский
Для конечной Z-группы G и непустой группы коммутатор подгруппа является proper подгруппой.
LaTeX
$$\( \text{If } G \text{ is finite } G \text{ is a } Z\text{-group, and } G \text{ is nontrivial, then } [G,G] < G. \)$$
Lean4
theorem commutator_lt [Finite G] [IsZGroup G] [Nontrivial G] : commutator G < ⊤ :=
by
let p := (Nat.card G).minFac
have hp : p.Prime := Nat.minFac_prime Finite.one_lt_card.ne'
have := Fact.mk hp
let P : Sylow p G := default
have hP := isZGroup p hp P
let f := MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)
refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_
have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd
contrapose! h
rw [← Subgroup.isComplement'_top_left, ← (not_lt_top_iff.mp h)]
exact hP.isComplement' rfl
