instIsCyclicSubtypeMemSubgroupOfFactPrime

Mathlib.GroupTheory.SpecificGroups.ZGroup

URI: https://scilib.ai/kg/mathlib#IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime

English

For any prime p, the Sylow p-subgroup of a Z-group is cyclic.

Русский

Для любого простого p, подгруппа Силовой p Z-группы циклична.

LaTeX

$$$\forall p\text{ prime},\ IsCyclic(\mathrm{Sylow}_p(G))$$$

Lean4

instance [IsZGroup G] {p : ℕ} [Fact p.Prime] (P : Sylow p G) : IsCyclic P :=
  isZGroup p Fact.out P

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru