derivedSeries_normal — Mathlib

English

For every n, the subgroup derivedSeries(G,n) is a normal subgroup of G.

Русский

Для каждого n подгруппа derivedSeries(G,n) нормальна в G.

LaTeX

$$$(\\mathrm{derivedSeries}(G,n)) \\trianglelefteq G$$$

Lean4

theorem derivedSeries_normal (n : ℕ) : (derivedSeries G n).Normal := by
  induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

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