isCyclic_of_isZGroup — Mathlib

English

Let G be a group in which every finite subgroup is cyclic. Then any p-subgroup P of G is cyclic.

Русский

Пусть G — группа, каждая конечная подгруппа которой циклична. Тогда любая p-подгруппа P группы G циклична.

LaTeX

$$$\forall G\,[Group\ G]\,[IsZGroup\ G]\,\forall p\in\mathbb N\,\forall P\subseteq G\,\bigl(\text{IsPGroup } p\ P\bigr)\Rightarrow \text{IsCyclic } P$$$

Lean4

theorem _root_.IsPGroup.isCyclic_of_isZGroup [IsZGroup G] {p : ℕ} [Fact p.Prime] {P : Subgroup G} (hP : IsPGroup p P) :
    IsCyclic P := by
  obtain ⟨Q, hQ⟩ := hP.exists_le_sylow
  exact Subgroup.isCyclic_of_le hQ

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