basic): `normalizer_eq_top` (#9917)

Commit

4 years ago

feat(group_theory/subgroup/basic): `normalizer_eq_top` (#9917) The normalizer is the whole group if and only if the subgroup is normal.

Author

tb65536

Parents