chore(group_theory/quotient_group): Tag lemmas with @[to_additive] (#…

…9771) Adds `@[to_additive]` to a couple lemmas.
leanprover-community · Oct 17, 2021 · 7aa431c · 7aa431c
1 parent a1a05ad
commit 7aa431c
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
@@ -414,11 +414,12 @@ end third_iso_thm
 
 section trivial
 
-lemma subsingleton_quotient_top : subsingleton (quotient_group.quotient (⊤ : subgroup G)) :=
+@[to_additive] lemma subsingleton_quotient_top :
+  subsingleton (quotient_group.quotient (⊤ : subgroup G)) :=
 trunc.subsingleton
 
 /-- If the quotient by a subgroup gives a singleton then the subgroup is the whole group. -/
-lemma subgroup_eq_top_of_subsingleton (H : subgroup G)
+@[to_additive] lemma subgroup_eq_top_of_subsingleton (H : subgroup G)
   (h : subsingleton (quotient_group.quotient H)) : H = ⊤ :=
 top_unique $ λ x _,
   have this : 1⁻¹ * x ∈ H := quotient_group.eq.1 (subsingleton.elim _ _),