mathlib3

251bd842 - feat(group_theory/subgroup/basic): One more `mem_normalizer_iff` lemma (#13395)

feat(group_theory/subgroup/basic): One more `mem_normalizer_iff` lemma (#13395) This PR golfs `mem_normalizer_iff'` and adds `mem_normalizer_iff''`. There are not so easy to deduce from each other, so it's nice to have these variations available.