derived_le_lower_central — Mathlib

English

For every natural number n, the nth derived subgroup is contained in the nth lower central subgroup.

Русский

Для каждого n-й производной подпгруппы выполняется включение в n-ю нижнюю центральную подпгруппу.

LaTeX

$$$\\text{derivedSeries}(G,n) \\le \\text{lowerCentralSeries}(G,n)$$$

Lean4

theorem derived_le_lower_central (n : ℕ) : derivedSeries G n ≤ lowerCentralSeries G n := by
  induction n with
  | zero => simp
  | succ i ih => apply commutator_mono ih; simp

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