From 7aa431c95730c8f90955d08b38ae2c548a12e0d1 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sun, 17 Oct 2021 03:34:30 +0000 Subject: [PATCH] chore(group_theory/quotient_group): Tag lemmas with `@[to_additive]` (#9771) Adds `@[to_additive]` to a couple lemmas. --- src/group_theory/quotient_group.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean index 49a72e425c8df..9e8fe447971cd 100644 --- 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 _ _),