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.





leanprover-community/mathlib,leanprover-community/mathlib