Theorems · Definition · group theory

AddSubgroup.upperCentralSeriesStep

{G : Type u_1} → [inst : AddGroup G] → (N : AddSubgroup G) → [N.Normal] → AddSubgroup G

If N is a normal additive subgroup of G, then the set {x : G | ∀ y : G, x + y -x - y ∈ N} is an additive subgroup of G (because it is the preimage in G of the centre of the additive quotient group G/N.)

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

5 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext

Assumes

AddGroupAddSubgroup.Normal