lowerCentralSeries_normal — Mathlib

English

For every natural number n, the nth term of the lower central series is a normal subgroup of G.

Русский

Для любого натурального числа n члена γ_n(G) является нормальной подгруппой G.

LaTeX

$$$(\\lowerCentralSeries G\\,n) \\triangleleft G$$$

Lean4

instance lowerCentralSeries_normal (n : ℕ) : Normal (lowerCentralSeries G n) := by
  induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ d hd => exact @Subgroup.commutator_normal _ _ (lowerCentralSeries G d) ⊤ hd _

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