normal_subgroupOf — Mathlib

English

Same content as the previous item: the subgroup of a normal subgroup inside another subgroup remains normal.

Русский

То же самое: подгруппа нормальной подгруппы внутри другой подгруппы остаётся нормальной.

LaTeX

$$$ (N.subgroupOf H).Normal $$$

Lean4

@[to_additive]
instance (priority := 100) normal_subgroupOf {H N : Subgroup G} [N.Normal] : (N.subgroupOf H).Normal :=
  Subgroup.normal_comap _

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