Commit 2025-03-25 08:54 80c61f18

View on Github →

feat(Algebra/Group/Subgroup, GroupTheory/QuotientGroup): strengthen second isomorphism theorem for groups (#22650) The stronger statement is necessary when we wish that H and H ⊔ N in the statement _ ⧸ N.subgroupOf H ≃* _ ⧸ N.subgroupOf (H ⊔ N) may need to be of a type larger than whichever subgroup H is normal in. Furthermore, this commit adapts some basic results about Normal subgroups to be wrt subgroups of normalizers instead. Moves:

Subgroup.le_normalizer_of_normal -> Subgroup.le_normalizer_of_normal_subgroupOf

Estimated changes

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

modified theorem Subgroup.le_normalizer_of_normal

added theorem Subgroup.le_normalizer_of_normal_subgroupOf

added theorem Subgroup.normal_subgroupOf_of_le_normalizer

added theorem Subgroup.normal_subgroupOf_sup_of_le_normalizer

added theorem Subgroup.subset_normalizer_of_normal

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

added theorem Subgroup.coe_mul_of_left_le_normalizer_right

added theorem Subgroup.coe_mul_of_right_le_normalizer_left

modified theorem Subgroup.mul_normal

modified theorem Subgroup.normal_mul

modified theorem Subgroup.set_mul_normal_comm

added theorem Subgroup.set_mul_normalizer_comm

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean