isCyclic_right_of_prod

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

← MathLib Explorer

English

Let M and N be groups. If the direct product M × N is cyclic, then the factor N is cyclic.

Русский

Пусть M и N — группы. Если прямая сумма M × N циклическая, то N циклическая.

LaTeX

$$$IsCyclic(M \times N) \Rightarrow IsCyclic(N)$$$

Lean4

@[to_additive isAddCyclic_right_of_prod]
theorem isCyclic_right_of_prod : IsCyclic N :=
  isCyclic_of_surjective (MonoidHom.snd M N) Prod.snd_surjective

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

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

Разделы

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

Аффилиация

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