derivedSeries_characteristic — Mathlib

English

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

Русский

Для каждого n подгруппа derivedSeries(G,n) является характеристической подгруппой G.

LaTeX

$$$(\\mathrm{derivedSeries}(G,n)).\\text{Characteristic}$$$

Lean4

instance derivedSeries_characteristic (n : ℕ) : (derivedSeries G n).Characteristic := by
  induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _

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