isCyclic_of_injective

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

← MathLib Explorer

English

If α is cyclic, then any subgroup H ≤ α is cyclic.

Русский

Если α циклична, то любая подгруппа H ⊆ α циклична.

LaTeX

$$IsCyclic(α) ⇒ IsCyclic(H) for any H ≤ α$$

Lean4

@[to_additive]
theorem isCyclic_of_injective [IsCyclic G'] (f : G →* G') (hf : Function.Injective f) : IsCyclic G :=
  isCyclic_of_surjective (MonoidHom.ofInjective hf).symm (MonoidHom.ofInjective hf).symm.surjective

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

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

Разделы

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

Аффилиация

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