instNormalUpperCentralSeriesStep — Mathlib

English

The subgroup upperCentralSeriesStep(H) is a normal subgroup of G; this follows from its identification as a comap of the center in G/H.

Русский

Подгруппа upperCentralSeriesStep(H) нормальна в G; это следует из её идентификации как предобраза центра в G/H.

LaTeX

$$$(\\operatorname{upperCentralSeriesStep}(H)).Normal$$$

Lean4

instance : Normal (upperCentralSeriesStep H) :=
  by
  rw [upperCentralSeriesStep_eq_comap_center]
  infer_instance

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