Theorems · Definition · group theory

Subgroup.normalizer

{G : Type u_1} → [inst : Group G] → Set G → Subgroup G

The normalizer of S is the subgroup of G whose elements satisfy g * S * g⁻¹ = S. When S is a subgroup, this is the largest subgroup of G inside which S is normal.

Defined in

Mathlib.Algebra.Group.Subgroup.Defs

Cited by

108 results in Mathlib

Foundations

Depth 13 from the axioms, rests on 69 definitions · uses propext, Quot.sound

Assumes

Group