subgroupOf

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.Normal.subgroupOf

English

If H is normal in G, then H.subgroupOf K is normal in G for any K ≤ G.

Русский

Если H нормальна в G, то H.subgroupOf K нормальна в G для любой K ⊆ G.

LaTeX

$$$ (H.subgroupOf K) \\trianglelefteq G $$$

Lean4

@[to_additive]
theorem subgroupOf {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) : (H.subgroupOf K).Normal :=
  hH.comap _

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

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

Разделы

Аффилиация

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