feat(Algebra/Category/GroupCat/Injective) : commutative multiplicativ…

…e groups have enough injectives (#8819)

since commutative additive groups have enough injectives, multiplicative ones have enough injectives as well.

Mathlib/Algebra/Category/GroupCat/Injective.lean

@@ -5,6 +5,7 @@ Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Category.GroupCat.EpiMono
 import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
+import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Module.Injective
 import Mathlib.Topology.Instances.AddCircle
 import Mathlib.Topology.Instances.Rat
@@ -21,7 +22,10 @@ groups and that the category of abelian groups has enough injective objects.
 ## Main results
 
 - `AddCommGroupCat.injective_of_divisible` : a divisible group is also an injective object.
-- `AddCommGroupCat.enoughInjectives` : the category of abelian groups has enough injectives.
+- `AddCommGroupCat.enoughInjectives` : the category of abelian groups (written additively) has
+  enough injectives.
+- `CommGroupCat.enoughInjectives` : the category of abelian group (written multiplicatively) has
+  enough injectives.
 
 ## Implementation notes
 
@@ -167,7 +171,14 @@ lemma toNext_inj : Function.Injective <| toNext A_ :=
 
 end enough_injectives_aux_proofs
 
-instance enoughInjectives : EnoughInjectives (AddCommGroupCat.{u}) where
+instance enoughInjectives : EnoughInjectives AddCommGroupCat.{u} where
   presentation A_ := ⟨enough_injectives_aux_proofs.presentation A_⟩
 
 end AddCommGroupCat
+
+namespace CommGroupCat
+
+instance enoughInjectives : EnoughInjectives CommGroupCat.{u} :=
+  EnoughInjectives.of_equivalence commGroupAddCommGroupEquivalence.functor
+
+end CommGroupCat