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 · Oct 25, 2021 · bfcbe68 · bfcbe68
1 parent 41b90d7
commit bfcbe68
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
@@ -1132,6 +1132,10 @@ variable {H}
 instance normal_in_normalizer : (H.comap H.normalizer.subtype).normal :=
 ⟨λ x xH g, by simpa using (g.2 x).1 xH⟩
 
+@[to_additive] lemma normalizer_eq_top : H.normalizer = ⊤ ↔ H.normal :=
+eq_top_iff.trans ⟨λ h, ⟨λ a ha b, (h (mem_top b) a).mp ha⟩, λ h a ha b,
+  ⟨λ hb, h.conj_mem b hb a, λ hb, by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩
+
 open_locale classical
 
 @[to_additive]