Commit 2025-03-14 18:40 f47e8d64

View on Github →

refactor(Algebra/Group/Subgroup/Basic): clean up normalizer lemmas (#22913) This PR cleans up several normalizer lemmas in Algebra/Group/Subgroup/Basic. Several lemmas had unnecessary assumptions or unnecessarily complicated proofs.

Estimated changes

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

deleted theorem Subgroup.comap_normalizer_eq_of_injective_of_le_range

added theorem Subgroup.comap_normalizer_eq_of_le_range

added theorem Subgroup.inf_normalizer_le_normalizer_inf

modified theorem Subgroup.inf_subgroupOf_inf_normal_of_left

modified theorem Subgroup.inf_subgroupOf_inf_normal_of_right

added theorem Subgroup.normal_subgroupOf_iff_le_normalizer

added theorem Subgroup.normal_subgroupOf_iff_le_normalizer_inf

modified theorem Subgroup.subgroupOf_normalizer_eq

Modified Mathlib/GroupTheory/Sylow.lean