normal_in_normalizer

Mathlib.Algebra.Group.Subgroup.Basic

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

← MathLib Explorer

English

The subgroup (H.subgroupOf H.normalizer) is normal in H.normalizer.

Русский

Подгруппа (H.subgroupOf H.normalizer) нормальна в H.normalizer.

LaTeX

$$$\,(H.\mathrm{subgroupOf} H.\mathrm{normalizer}).Normal$$$

Lean4

@[to_additive]
instance (priority := 100) normal_in_normalizer : (H.subgroupOf H.normalizer).Normal :=
  (normal_subgroupOf_iff_le_normalizer H.le_normalizer).mpr le_rfl

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

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

Разделы

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

Аффилиация

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