chore(algebra/order/sub): split file (#16868)

- [x] depends on: #16861

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/algebra/order/group.lean → src/algebra/order/group/basic.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.abs
-import algebra.order.sub
+import algebra.order.sub.basic
 import algebra.order.monoid.min_max
 import algebra.order.monoid.prod
-import algebra.order.monoid.type_tags
 import algebra.order.monoid.units
+import algebra.order.monoid.order_dual
+import algebra.order.monoid.with_top
 
 /-!
 # Ordered groups
@@ -1337,26 +1338,6 @@ instance [ordered_comm_group G] [ordered_comm_group H] :
 
 end prod
 
-section type_tags
-
-instance [ordered_add_comm_group α] : ordered_comm_group (multiplicative α) :=
-{ ..multiplicative.comm_group,
-  ..multiplicative.ordered_comm_monoid }
-
-instance [ordered_comm_group α] : ordered_add_comm_group (additive α) :=
-{ ..additive.add_comm_group,
-  ..additive.ordered_add_comm_monoid }
-
-instance [linear_ordered_add_comm_group α] : linear_ordered_comm_group (multiplicative α) :=
-{ ..multiplicative.linear_order,
-  ..multiplicative.ordered_comm_group }
-
-instance [linear_ordered_comm_group α] : linear_ordered_add_comm_group (additive α) :=
-{ ..additive.linear_order,
-  ..additive.ordered_add_comm_group }
-
-end type_tags
-
 section norm_num_lemmas
 /- The following lemmas are stated so that the `norm_num` tactic can use them with the
 expected signatures.  -/

src/algebra/order/group/type_tags.lean

@@ -0,0 +1,27 @@
+/-
+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 algebra.order.group.basic
+import algebra.order.monoid.type_tags
+
+/-! # Ordered group structures on `multiplicative α` and `additive α`. -/
+
+variables {α : Type*}
+
+instance [ordered_add_comm_group α] : ordered_comm_group (multiplicative α) :=
+{ ..multiplicative.comm_group,
+  ..multiplicative.ordered_comm_monoid }
+
+instance [ordered_comm_group α] : ordered_add_comm_group (additive α) :=
+{ ..additive.add_comm_group,
+  ..additive.ordered_add_comm_monoid }
+
+instance [linear_ordered_add_comm_group α] : linear_ordered_comm_group (multiplicative α) :=
+{ ..multiplicative.linear_order,
+  ..multiplicative.ordered_comm_group }
+
+instance [linear_ordered_comm_group α] : linear_ordered_add_comm_group (additive α) :=
+{ ..additive.linear_order,
+  ..additive.ordered_add_comm_group }

src/algebra/order/lattice_group.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
 import algebra.group_power.basic -- Needed for squares
-import algebra.order.group
+import algebra.order.group.basic
 import tactic.nth_rewrite
 
 /-!

src/algebra/order/monoid/canonical.lean

@@ -7,7 +7,7 @@ import algebra.order.monoid.basic
 import order.min_max
 
 /-!
-# Canonical ordered monoids
+# Canonically ordered monoids
 -/
 
 universe u

src/algebra/order/ring.lean

@@ -6,7 +6,8 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 import algebra.char_zero.defs
 import algebra.ring.divisibility
 import algebra.hom.ring
-import algebra.order.group
+import algebra.order.group.basic
+import algebra.order.sub.canonical
 import algebra.order.ring_lemmas
 
 /-!