Theorems · Definition · group theory

Subgroup.upperCentralSeries

(G : Type u_1) → [inst : Group G] → ℕ → Subgroup G

upperCentralSeries G n is the nth 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.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

51 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group