normal_of_comm

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.normal_of_comm

English

In a commutative group, every subgroup is normal.

Русский

В коммутативной группе любая подгруппа является нормальной.

LaTeX

$$$\forall H \le G,\ H \text{ is normal in } G \quad \text{if } G \text{ is abelian}$$$

Lean4

@[to_additive]
instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
  ⟨by simp [mul_comm]⟩

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

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

Разделы

Аффилиация

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