Theorems · Definition · group theory

Subgroup.upperCentralSeriesStep

{G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [N.Normal] → Subgroup G

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

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

8 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext

Assumes

GroupSubgroup.Normal