English
A sequence H(n) of subgroups is descending central if H(0)=G and for all x ∈ G, n, x ∈ H(n) implies ∀ g ∈ G, x g x^{-1} g^{-1} ∈ H(n+1).
Русский
Последовательность подгрупп H(n) спускается по центральной серии: H(0)=G и если x ∈ H(n), то для всех g ∈ G коммутатор ∈ H(n+1).
LaTeX
$$$\text{IsDescendingCentralSeries}(H) := H(0)=G \wedge \forall x\in G,\forall n, x\in H(n)\Rightarrow \forall g\in G, xgx^{-1}g^{-1}\in H(n+1).$$$
Lean4
/-- A sequence of subgroups of `G` is a descending central series if `H 0` is `G` and
`⁅H n, G⁆ ⊆ H (n + 1)` for all `n`. Note that we do not require that `H n = {1}` for some `n`. -/
def IsDescendingCentralSeries (H : ℕ → Subgroup G) :=
H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ g, x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
