English
Let G be a group and n a natural number. Then the (n+1)th term of the lower central series of G equals the closure of all commutators formed by an element from the nth term with any element of G.
Русский
Пусть G — группа, и n — натуральное число. Тогда (n+1)-ая членная нижней центральной серийной последовательности G равна замыканию всех коммутаторов вида pqp^{-1}q^{-1}, где p ∈ γ_n(G), q ∈ G.
LaTeX
$$$\\displaystyle \\lowerCentralSeries G (n+1) = \\operatorname{closure}\\{ x \\mid \\exists p \\in \\lowerCentralSeries G n, \\exists q \\in G,\\ p q p^{-1} q^{-1} = x \\}$$$
Lean4
theorem lowerCentralSeries_succ (n : ℕ) :
lowerCentralSeries G (n + 1) =
closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ (⊤ : Subgroup G), p * q * p⁻¹ * q⁻¹ = x} :=
rfl
