isCyclic_multiplicative_iff

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

English

For a SubNegMonoid α, IsCyclic(Multiplicative α) iff IsAddCyclic α.

Русский

Для SubNegMonoid α, IsCyclic(Multiplicative α) эквивалентно IsAddCyclic α.

LaTeX

$$$$\\operatorname{IsCyclic}(\\operatorname{Multiplicative}\\alpha) \\iff \\operatorname{IsAddCyclic}\\alpha.$$$$

Lean4

@[simp]
theorem isCyclic_multiplicative_iff [SubNegMonoid α] : IsCyclic (Multiplicative α) ↔ IsAddCyclic α :=
  ⟨fun H ↦ ⟨H.1⟩, fun H ↦ ⟨H.1⟩⟩

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

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

Разделы

Аффилиация

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