feat(group_theory/subgroup) top is a normal subgroup (#4982)

leanprover-community · Nov 12, 2020 · 3f575d7 · 3f575d7
1 parent 509a224
commit 3f575d7
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean
@@ -747,6 +747,9 @@ end normal
 @[priority 100, to_additive]
 instance bot_normal : normal (⊥ : subgroup G) := ⟨by simp⟩
 
+@[priority 100, to_additive]
+instance top_normal : normal (⊤ : subgroup G) := ⟨λ _ _, mem_top⟩
+
 variable (G)
 /-- The center of a group `G` is the set of elements that commute with everything in `G` -/
 @[to_additive "The center of a group `G` is the set of elements that commute with everything in `G`"]