instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic

Mathlib.GroupTheory.SpecificGroups.Cyclic

URI: https://scilib.ai/kg/mathlib#instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic

English

A cyclic subgroup is abelian; this holds generally inside group theory.

Русский

Циклическая подгруппа — абелева; это справедливо в общей теории групп.

LaTeX

$$$$\\text{If } H \\text{ is cyclic (as a subgroup), then } H \\text{ is commutative (abelian).}$$$$

Lean4

instance [Group G] (H : Subgroup G) [IsCyclic H] : IsMulCommutative H :=
  ⟨IsCyclic.commutative⟩

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

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

Разделы

Аффилиация

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