instIsCyclicOfFiniteOfIsNilpotent

English

If a finite group G is Z-group and nilpotent, then G is cyclic.

Русский

Если конечная группа G является Z-группой и нильпотентна, то G циклична.

LaTeX

$$\( \text{If } G \\text{ finite and } G \\text{ is a } Z\text{-group and } G \\text{ is nilpotent, then } G \\text{ is cyclic}.$$

Lean4

instance [Finite G] [IsZGroup G] [hG : Group.IsNilpotent G] : IsCyclic G :=
  by
  have (p : { x // x ∈ (Nat.card G).primeFactors }) : Fact p.1.Prime := ⟨Nat.prime_of_mem_primeFactors p.2⟩
  obtain ⟨ϕ⟩ := ((isNilpotent_of_finite_tfae (G := G)).out 0 4).mp hG
  let _ : CommGroup G := ⟨fun g h ↦ by rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]⟩
  exact IsCyclic.of_exponent_eq_card (exponent_eq_card G)

Похожие утверждения