upperCentralSeries_mono — Mathlib

English

The sequence upperCentralSeries(G) is monotone in n: each term is contained in the next.

Русский

Последовательность upperCentralSeries(G) монотонна по индексу: каждая ступень включена в следующую.

LaTeX

$$$\forall n,\ \mathrm{upperCentralSeries}(G,n)\le\mathrm{upperCentralSeries}(G,n+1).$$$

Lean4

theorem upperCentralSeries_mono : Monotone (upperCentralSeries G) :=
  by
  refine monotone_nat_of_le_succ ?_
  intro n x hx y
  rw [mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]
  exact mul_mem hx (Normal.conj_mem (upperCentralSeries_normal G n) x⁻¹ (inv_mem hx) y)

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