upperCentralSeries_normal

Mathlib.GroupTheory.Nilpotent

URI: https://scilib.ai/kg/mathlib#upperCentralSeries_normal

English

Every term of the upper central series is a normal subgroup of the ambient group G.

Русский

Каждая члена верхней центральной серии нормальна в группе G.

LaTeX

$$$\forall n,\ (\mathrm{upperCentralSeries}(G,n))\lhd G.$$$

Lean4

instance upperCentralSeries_normal (n : ℕ) : Normal (upperCentralSeries G n) :=
  (upperCentralSeriesAux G n).2

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

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

Разделы

Аффилиация

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