of_squarefree — Mathlib

English

If a group has squarefree order, then it is a Z-group (every finite subgroup is cyclic).

Русский

Если порядок группы квадратно-безповторной, то она является Z-группой (каждая конечная подгруппа циклична).

LaTeX

$$$\operatorname{Squarefree}(|G|) \Rightarrow IsZGroup\ G$$$

Lean4

theorem of_squarefree (hG : Squarefree (Nat.card G)) : IsZGroup G :=
  by
  have : Finite G := Nat.finite_of_card_ne_zero hG.ne_zero
  refine ⟨fun p hp P ↦ ?_⟩
  have := Fact.mk hp
  obtain ⟨k, hk⟩ := P.2.exists_card_eq
  exact isCyclic_of_card_dvd_prime ((hk ▸ hG.pow_dvd_of_pow_dvd) P.card_subgroup_dvd_card)

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