instOfIsCyclic

Mathlib.GroupTheory.SpecificGroups.ZGroup

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

English

If G is cyclic, then G is a ZGroup.

Русский

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

LaTeX

$$$IsCyclic(G) \Rightarrow IsZGroup(G)$$$

Lean4

instance [IsCyclic G] : IsZGroup G :=
  ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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