[Merged by Bors] - feat: port Algebra.Order.Group.TypeTags

Mathlib.lean

@@ -42,6 +42,7 @@ import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Algebra.Order.Group.OrderIso
+import Mathlib.Algebra.Order.Group.TypeTags
 import Mathlib.Algebra.Order.Group.Units
 import Mathlib.Algebra.Order.Hom.Basic
 import Mathlib.Algebra.Order.Monoid.Basic

Mathlib/Algebra/Group/TypeTags.lean

@@ -368,10 +368,10 @@ instance Additive.addGroup [Group α] : AddGroup (Additive α) :=
 instance Multiplicative.group [AddGroup α] : Group (Multiplicative α) :=
   { Multiplicative.divInvMonoid with mul_left_inv := @add_left_neg α _ }
 
-instance [CommGroup α] : AddCommGroup (Additive α) :=
+instance Additive.addCommGroup [CommGroup α] : AddCommGroup (Additive α) :=
   { Additive.addGroup, Additive.addCommMonoid with }
 
-instance [AddCommGroup α] : CommGroup (Multiplicative α) :=
+instance Multiplicative.commGroup [AddCommGroup α] : CommGroup (Multiplicative α) :=
   { Multiplicative.group, Multiplicative.commMonoid with }
 
 /-- Reinterpret `α →+ β` as `Multiplicative α →* Multiplicative β`. -/

Mathlib/Algebra/Order/Group/TypeTags.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
+-/
+import Mathlib.Algebra.Order.Group.Instances
+import Mathlib.Algebra.Order.Monoid.TypeTags
+
+/-! # Ordered group structures on `multiplicative α` and `additive α`. -/
+
+
+variable {α : Type _} --[LinearOrderedAddCommGroup α]
+
+instance Multiplicative.orderedCommGroup [OrderedAddCommGroup α] :
+    OrderedCommGroup (Multiplicative α) :=
+  { Multiplicative.commGroup, Multiplicative.orderedCommMonoid with }
+
+instance Additive.orderedAddCommGroup [OrderedCommGroup α] :
+    OrderedAddCommGroup (Additive α) :=
+  { Additive.addCommGroup, Additive.orderedAddCommMonoid with }
+
+instance Multiplicative.linearOrderedCommGroup [LinearOrderedAddCommGroup α] :
+    LinearOrderedCommGroup (Multiplicative α) :=
+  { Multiplicative.linearOrder, Multiplicative.orderedCommGroup with }
+
+instance Additive.linearOrderedAddCommGroup [LinearOrderedCommGroup α] :
+    LinearOrderedAddCommGroup (Additive α) :=
+  { Additive.linearOrder, Additive.orderedAddCommGroup with }