chore(group_theory/quotient_group): drop unneeded names in `to_additi…

…ve` (#17821)

This only changes the names of `group` and `comm_group` instances.

src/group_theory/quotient_group.lean

@@ -56,12 +56,10 @@ protected def con : con G :=
     ... ∈ N : N.mul_mem (nN.conj_mem _ hab _) hcd
   end }
 
-@[to_additive quotient_add_group.add_group]
-instance quotient.group : group (G ⧸ N) :=
-(quotient_group.con N).group
+@[to_additive] instance quotient.group : group (G ⧸ N) := (quotient_group.con N).group
 
 /-- The group homomorphism from `G` to `G/N`. -/
-@[to_additive quotient_add_group.mk' "The additive group homomorphism from `G` to `G/N`."]
+@[to_additive "The additive group homomorphism from `G` to `G/N`."]
 def mk' : G →* G ⧸ N := monoid_hom.mk' (quotient_group.mk) (λ _ _, rfl)
 
 @[simp, to_additive]
@@ -89,19 +87,18 @@ See note [partially-applied ext lemmas]. "-/]
 lemma monoid_hom_ext ⦃f g : G ⧸ N →* H⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
 monoid_hom.ext $ λ x, quotient_group.induction_on x $ (monoid_hom.congr_fun h : _)
 
-@[simp, to_additive quotient_add_group.eq_zero_iff]
+@[simp, to_additive]
 lemma eq_one_iff {N : subgroup G} [nN : N.normal] (x : G) : (x : G ⧸ N) = 1 ↔ x ∈ N :=
 begin
   refine quotient_group.eq.trans _,
   rw [mul_one, subgroup.inv_mem_iff],
 end
 
-@[simp, to_additive quotient_add_group.ker_mk]
-lemma ker_mk :
-  monoid_hom.ker (quotient_group.mk' N : G →* G ⧸ N) = N :=
+@[simp, to_additive]
+lemma ker_mk : monoid_hom.ker (quotient_group.mk' N : G →* G ⧸ N) = N :=
 subgroup.ext eq_one_iff
 
-@[to_additive quotient_add_group.eq_iff_sub_mem]
+@[to_additive]
 lemma eq_iff_div_mem {N : subgroup G} [nN : N.normal] {x y : G} :
   (x : G ⧸ N) = y ↔ x / y ∈ N :=
 begin
@@ -112,8 +109,8 @@ end
 -- for commutative groups we don't need normality assumption
 omit nN
 
-@[to_additive quotient_add_group.add_comm_group]
-instance {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) :=
+@[to_additive]
+instance quotient.comm_group {G : Type*} [comm_group G] (N : subgroup G) : comm_group (G ⧸ N) :=
 { mul_comm := λ a b, quotient.induction_on₂' a b
     (λ a b, congr_arg mk (mul_comm a b)),
   .. @quotient_group.quotient.group _ _ N N.normal_of_comm }
@@ -122,50 +119,37 @@ include nN
 
 local notation ` Q ` := G ⧸ N
 
-@[simp, to_additive quotient_add_group.coe_zero]
-lemma coe_one : ((1 : G) : Q) = 1 := rfl
-
-@[simp, to_additive quotient_add_group.coe_add]
-lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
-
-@[simp, to_additive quotient_add_group.coe_neg]
-lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
-
-@[simp, to_additive quotient_add_group.coe_sub]
-lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl
-
-@[simp, to_additive quotient_add_group.coe_nsmul]
-lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl
-
-@[simp, to_additive quotient_add_group.coe_zsmul]
-lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl
+@[simp, to_additive] lemma coe_one : ((1 : G) : Q) = 1 := rfl
+@[simp, to_additive] lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
+@[simp, to_additive] lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
+@[simp, to_additive] lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := rfl
+@[simp, to_additive] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := rfl
+@[simp, to_additive] lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := rfl
 
 /-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
 group homomorphism `G/N →* H`. -/
-@[to_additive quotient_add_group.lift "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)`
-descends (i.e. `lift`s) to a group homomorphism `G/N →* H`."]
+@[to_additive "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
+to a group homomorphism `G/N →* H`."]
 def lift (φ : G →* H) (HN : ∀x∈N, φ x = 1) : Q →* H :=
 (quotient_group.con N).lift φ $ λ x y h, begin
   simp only [quotient_group.con, left_rel_apply, con.rel_mk] at h,
   calc φ x = φ (y * (x⁻¹ * y)⁻¹) : by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
        ... = φ y                 : by rw [φ.map_mul, HN _ (N.inv_mem h), mul_one]
   end
 
-@[simp, to_additive quotient_add_group.lift_mk]
-lemma lift_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (g : Q) = φ g := rfl
+@[simp, to_additive]
+lemma lift_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (g : Q) = φ g := rfl
 
-@[simp, to_additive quotient_add_group.lift_mk']
-lemma lift_mk' {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
-  lift N φ HN (mk g : Q) = φ g := rfl
+@[simp, to_additive]
+lemma lift_mk' {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) : lift N φ HN (mk g : Q) = φ g := rfl
 
-@[simp, to_additive quotient_add_group.lift_quot_mk]
+@[simp, to_additive]
 lemma lift_quot_mk {φ : G →* H} (HN : ∀x∈N, φ x = 1) (g : G) :
   lift N φ HN (quot.mk _ g : Q) = φ g := rfl
 
 /-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
-@[to_additive quotient_add_group.map "An `add_group` homomorphism `f : G →+ H` induces a map
-`G/N →+ H/M` if `N ⊆ f⁻¹(M)`."]
+@[to_additive "An `add_group` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if
+`N ⊆ f⁻¹(M)`."]
 def map (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) :
   G ⧸ N →* H ⧸ M :=
 begin
@@ -176,13 +160,12 @@ begin
   exact h hx,
 end
 
-@[simp, to_additive quotient_add_group.map_coe] lemma map_coe
-  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+@[simp, to_additive] lemma map_coe (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f)
+  (x : G) :
   map N M f h ↑x = ↑(f x) :=
 lift_mk' _ _ x
 
-@[to_additive quotient_add_group.map_mk'] lemma map_mk'
-  (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
+@[to_additive] lemma map_mk' (M : subgroup H) [M.normal] (f : G →* H) (h : N ≤ M.comap f) (x : G) :
   map N M f h (mk' _ x) = ↑(f x) :=
 quotient_group.lift_mk' _ _ x
 
@@ -268,20 +251,17 @@ variables (φ : G →* H)
 open function monoid_hom
 
 /-- The induced map from the quotient by the kernel to the codomain. -/
-@[to_additive quotient_add_group.ker_lift "The induced map from the quotient by the kernel to the
-codomain."]
+@[to_additive "The induced map from the quotient by the kernel to the codomain."]
 def ker_lift : G ⧸ ker φ →* H :=
 lift _ φ $ λ g, φ.mem_ker.mp
 
-@[simp, to_additive quotient_add_group.ker_lift_mk]
-lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g :=
-lift_mk _ _ _
+@[simp, to_additive]
+lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g := lift_mk _ _ _
 
-@[simp, to_additive quotient_add_group.ker_lift_mk']
-lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g :=
-lift_mk' _ _ _
+@[simp, to_additive]
+lemma ker_lift_mk' (g : G) : (ker_lift φ) (mk g) = φ g := lift_mk' _ _ _
 
-@[to_additive quotient_add_group.ker_lift_injective]
+@[to_additive]
 lemma ker_lift_injective : injective (ker_lift φ) :=
 assume a b, quotient.induction_on₂' a b $
   assume a b (h : φ a = φ b), quotient.sound' $
@@ -291,19 +271,18 @@ assume a b, quotient.induction_on₂' a b $
 -- so there is a bit of annoying code duplication here
 
 /-- The induced map from the quotient by the kernel to the range. -/
-@[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to
-the range."]
+@[to_additive "The induced map from the quotient by the kernel to the range."]
 def range_ker_lift : G ⧸ ker φ →* φ.range :=
 lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa ker_range_restrict
 
-@[to_additive quotient_add_group.range_ker_lift_injective]
+@[to_additive]
 lemma range_ker_lift_injective : injective (range_ker_lift φ) :=
 assume a b, quotient.induction_on₂' a b $
   assume a b (h : φ.range_restrict a = φ.range_restrict b), quotient.sound' $
   by rw [left_rel_apply, ←ker_range_restrict, mem_ker,
   φ.range_restrict.map_mul, ← h, φ.range_restrict.map_inv, inv_mul_self]
 
-@[to_additive quotient_add_group.range_ker_lift_surjective]
+@[to_additive]
 lemma range_ker_lift_surjective : surjective (range_ker_lift φ) :=
 begin
   rintro ⟨_, g, rfl⟩,
@@ -313,16 +292,15 @@ end
 
 /-- **Noether's first isomorphism theorem** (a definition): the canonical isomorphism between
 `G/(ker φ)` to `range φ`. -/
-@[to_additive quotient_add_group.quotient_ker_equiv_range "The first isomorphism theorem
-(a definition): the canonical isomorphism between `G/(ker φ)` to `range φ`."]
+@[to_additive "The first isomorphism theorem (a definition): the canonical isomorphism between
+`G/(ker φ)` to `range φ`."]
 noncomputable def quotient_ker_equiv_range : G ⧸ ker φ ≃* range φ :=
 mul_equiv.of_bijective (range_ker_lift φ) ⟨range_ker_lift_injective φ, range_ker_lift_surjective φ⟩
 
 /-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
 with a right inverse `ψ : H → G`. -/
-@[to_additive quotient_add_group.quotient_ker_equiv_of_right_inverse "The canonical isomorphism
-`G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H` with a right inverse `ψ : H → G`.",
-  simps]
+@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a homomorphism `φ : G →+ H`
+with a right inverse `ψ : H → G`.", simps]
 def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inverse ψ φ) :
   G ⧸ ker φ ≃* H :=
 { to_fun := ker_lift φ,
@@ -332,16 +310,15 @@ def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inv
   .. ker_lift φ }
 
 /-- The canonical isomorphism `G/⊥ ≃* G`. -/
-@[to_additive quotient_add_group.quotient_bot "The canonical isomorphism `G/⊥ ≃+ G`.", simps]
+@[to_additive "The canonical isomorphism `G/⊥ ≃+ G`.", simps]
 def quotient_bot : G ⧸ (⊥ : subgroup G) ≃* G :=
 quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id (λ x, rfl)
 
 /-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.
 
 For a `computable` version, see `quotient_group.quotient_ker_equiv_of_right_inverse`.
 -/
-@[to_additive quotient_add_group.quotient_ker_equiv_of_surjective "The canonical isomorphism
-`G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
+@[to_additive "The canonical isomorphism `G/(ker φ) ≃+ H` induced by a surjection `φ : G →+ H`.
 
 For a `computable` version, see `quotient_add_group.quotient_ker_equiv_of_right_inverse`."]
 noncomputable def quotient_ker_equiv_of_surjective (hφ : function.surjective φ) :
@@ -495,29 +472,29 @@ nM.map _ mk_surjective
 variables (h : N ≤ M)
 
 /-- The map from the third isomorphism theorem for groups: `(G / N) / (M / N) → G / M`. -/
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux
-"The map from the third isomorphism theorem for additive groups: `(A / N) / (M / N) → A / M`."]
+@[to_additive "The map from the third isomorphism theorem for additive groups:
+`(A / N) / (M / N) → A / M`."]
 def quotient_quotient_equiv_quotient_aux :
   (G ⧸ N) ⧸ (M.map (mk' N)) →* G ⧸ M :=
 lift (M.map (mk' N))
   (map N M (monoid_hom.id G) h)
   (by { rintro _ ⟨x, hx, rfl⟩, rw map_mk' N M _ _ x,
         exact (quotient_group.eq_one_iff _).mpr hx })
 
-@[simp, to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe]
+@[simp, to_additive]
 lemma quotient_quotient_equiv_quotient_aux_coe (x : G ⧸ N) :
   quotient_quotient_equiv_quotient_aux N M h x = quotient_group.map N M (monoid_hom.id G) h x :=
 quotient_group.lift_mk' _ _ x
 
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe]
+@[to_additive]
 lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) :
   quotient_quotient_equiv_quotient_aux N M h (x : G ⧸ N) =
     x :=
 quotient_group.lift_mk' _ _ x
 
-/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃ G / M`. -/
-@[to_additive quotient_add_group.quotient_quotient_equiv_quotient
-"**Noether's third isomorphism theorem** for additive groups: `(A / N) / (M / N) ≃ A / M`."]
+/-- **Noether's third isomorphism theorem** for groups: `(G / N) / (M / N) ≃* G / M`. -/
+@[to_additive "**Noether's third isomorphism theorem** for additive groups:
+`(A / N) / (M / N) ≃+ A / M`."]
 def quotient_quotient_equiv_quotient :
   (G ⧸ N) ⧸ (M.map (quotient_group.mk' N)) ≃* G ⧸ M :=
 monoid_hom.to_mul_equiv
@@ -548,7 +525,7 @@ top_unique $ λ x _,
 
 end trivial
 
-@[to_additive quotient_add_group.comap_comap_center]
+@[to_additive]
 lemma comap_comap_center {H₁ : subgroup G} [H₁.normal] {H₂ : subgroup (G ⧸ H₁)} [H₂.normal] :
   (((subgroup.center ((G ⧸ H₁) ⧸ H₂))).comap (mk' H₂)).comap (mk' H₁) =
   (subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) :=

src/linear_algebra/quotient.lean

@@ -62,7 +62,7 @@ instance : inhabited (M ⧸ p) := ⟨0⟩
 by simpa using (quotient.eq p : mk x = 0 ↔ _)
 
 instance add_comm_group : add_comm_group (M ⧸ p) :=
-quotient_add_group.add_comm_group p.to_add_subgroup
+quotient_add_group.quotient.add_comm_group p.to_add_subgroup
 
 @[simp] theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y := rfl