normal_subgroupOf_sup_of_le_normalizer

Mathlib.Algebra.Group.Subgroup.Basic

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

← MathLib Explorer

English

If H ≤ N.normalizer, then N.subgroupOf (H ⊔ N) is normal.

Русский

Если H ≤ N.normalizer, то N.subgroupOf (H ⊔ N) нормальна.

LaTeX

$$H \le N.normalizer ⇒ (N.subgroupOf (H \vee N)).Normal$$

Lean4

@[to_additive]
theorem normal_subgroupOf_sup_of_le_normalizer {H N : Subgroup G} (hLE : H ≤ N.normalizer) :
    (N.subgroupOf (H ⊔ N)).Normal :=
  by
  rw [normal_subgroupOf_iff_le_normalizer le_sup_right]
  exact sup_le hLE le_normalizer

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

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

Разделы

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

Аффилиация

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