instNormal

Mathlib.Topology.Algebra.OpenSubgroup

URI: https://scilib.ai/kg/mathlib#OpenNormalSubgroup.instNormal

English

If H is an open normal subgroup of G, then H is a normal subgroup of G.

Русский

Если H — открытая нормальная подгруппа G, то H является нормальной подгруппой G.

LaTeX

$$$H \\lhd G$$$

Lean4

@[to_additive]
instance (H : OpenNormalSubgroup G) : H.toSubgroup.Normal :=
  H.isNormal'

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

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

Разделы

Аффилиация

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