instSubtypeMemSubgroup

Mathlib.GroupTheory.SpecificGroups.ZGroup

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

English

If G is a Z-group, then any subgroup H ≤ G is also a Z-group.

Русский

Если G — Z-группа, то любая подгруппа H ≤ G тоже является Z-группой.

LaTeX

$$\( \text{If } G \text{ is a } Z\text{-group, then every subgroup } H \le G \text{ is a } Z\text{-group}.$$

Lean4

instance [IsZGroup G] (H : Subgroup G) : IsZGroup H :=
  of_injective H.subtype_injective

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

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

Разделы

Аффилиация

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