Commit 2026-04-07 10:05 1ddd02a3

View on Github →

feat(GroupTheory/Subgroup): basic API for set normalizers (#36760)

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added theorem AddSubgroup.mem_normalizer_iff_conj_image_eq

added theorem AddSubgroup.normalizer_le_normalizer_closure

added theorem CommGroup.normalizer_eq_top

added theorem Subgroup.maximal_normal_subgroupOf_normalizer

added theorem Subgroup.mem_normalizer_iff_conj_image_eq

added theorem Subgroup.normalizer_empty

added theorem Subgroup.normalizer_le_normalizer_closure

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

modified theorem Subgroup.mem_normalizer_iff''

modified theorem Subgroup.mem_normalizer_iff'

modified theorem Subgroup.mem_normalizer_iff

modified theorem Subgroup.mem_set_normalizer_iff''

modified theorem Subgroup.mem_set_normalizer_iff'

modified theorem Subgroup.mem_set_normalizer_iff

Modified Mathlib/GroupTheory/Commutator/Basic.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Subgroup/Center.lean

modified def Subgroup.center

modified theorem Subgroup.center_le_normalizer

Modified Mathlib/GroupTheory/Subgroup/Centralizer.lean

modified def Subgroup.centralizer

added theorem Subgroup.centralizer_le_normalizer

added theorem Subgroup.mem_centralizer_iff_commutator_eq_one'

added theorem Subgroup.normalizer_singleton