isCyclic_left_of_prod

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

← MathLib Explorer

English

If M × N is cyclic, then M is cyclic.

Русский

Если произведение M × N циклично, то M циклична.

LaTeX

$$IsCyclic M$$

Lean4

@[to_additive isAddCyclic_left_of_prod]
theorem isCyclic_left_of_prod : IsCyclic M :=
  isCyclic_of_surjective (MonoidHom.fst M N) Prod.fst_surjective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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