English
The nth term of the upper central series is the subgroup of G obtained as the first component of the auxiliary construction, i.e., upperCentralSeries G n = (upperCentralSeriesAux G n).fst.
Русский
Член p-й ступени верхней центральной серии группы G равен первой компоненты вспомогательного построения: upperCentralSeries G n = (upperCentralSeriesAux G n).fst.
LaTeX
$$$\mathrm{upperCentralSeries}(G,n)=(\mathrm{upperCentralSeriesAux}(G,n)).\mathrm{fst}$$$
Lean4
/-- `upperCentralSeries G n` is the `n`th term in the upper central series of `G`.
This is the increasing chain of subgroups of `G` that starts with the trivial subgroup `⊥` of `G`
and then continues defining `upperCentralSeries G (n + 1)` to be all the elements of `G`
that, modulo `upperCentralSeries G n`, belong to the center of the quotient
`G ⧸ upperCentralSeries G n`.
In particular, the identities
* `upperCentralSeries G 0 = ⊥` (`upperCentralSeries_zero`);
* `upperCentralSeries G 1 = center G` (`upperCentralSeries_one`);
hold.
-/
def upperCentralSeries (n : ℕ) : Subgroup G :=
(upperCentralSeriesAux G n).1
