le_normalizer_of_normal_subgroupOf

Mathlib.Algebra.Group.Subgroup.Basic

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

← MathLib Explorer

English

If H ≤ K and (H.subgroupOf K).Normal, then K ≤ H.normalizer.

Русский

Если H ≤ K и (H.subgroupOf K).Normal, то K ≤ H.normalizer.

LaTeX

$$$(H \le K) \land (H.\mathrm{subgroupOf}K).Normal \Rightarrow K \le H.\mathrm{normalizer}$$$

Lean4

@[to_additive]
theorem le_normalizer_of_normal_subgroupOf [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer :=
  (normal_subgroupOf_iff_le_normalizer HK).mp hK

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

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

Разделы

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

Аффилиация

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