Theorems · Definition · group theory

AddSubgroup.normalizer

{G : Type u_1} → [inst : AddGroup G] → Set G → AddSubgroup 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

59 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

AddGroup