feat(group_theory/subgroup/basic): `normalizer_eq_top` (#9917)
feat(group_theory/subgroup/basic): `normalizer_eq_top` (#9917)

The normalizer is the whole group if and only if the subgroup is normal.





leanprover-community/mathlib,leanprover-community/mathlib