English
Membership in the (n+1)-st term of the upper central series is characterized by a commutator condition: x ∈ upperCentralSeries(G, n+1) iff ∀ y ∈ G, x y x^{-1} y^{-1} ∈ upperCentralSeries(G,n).
Русский
Член x группы G принадлежит к (n+1)-й ступени верхней центральной серии тогда и только тогда, когда для всех y ∈ G коммутатор [x,y] лежит в upperCentralSeries(G,n).
LaTeX
$$$x\in \mathrm{upperCentralSeries}(G,n+1)\iff \forall y\in G,\ x\,y\,x^{-1}\,y^{-1}\in \mathrm{upperCentralSeries}(G,n).$$$
Lean4
/-- The `n+1`st term of the upper central series `H i` has underlying set equal to the `x` such
that `⁅x,G⁆ ⊆ H n`. -/
theorem mem_upperCentralSeries_succ_iff {n : ℕ} {x : G} :
x ∈ upperCentralSeries G (n + 1) ↔ ∀ y : G, x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n :=
Iff.rfl
