chore: move non @[to_additive] parts of Algebra.Order.Monoid and Algebra.Order.Group to a different file (#14667)

Following the discussion on #14598, move `LinearOrderedAddCommMonoidWithTop`, `LinearOrderedAddCommGroupWithTop`, and associated theorems to `Algebra.Order.AddGroupWithTop`.



Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

Author: Command-Master

Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Dvorak
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Order.BoundedOrder
 
 /-!
 # Do not combine OrderedCancelAddCommMonoid with BoundedOrder

Mathlib.lean

@@ -494,6 +494,7 @@ import Mathlib.Algebra.MvPolynomial.Variables
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue
+import Mathlib.Algebra.Order.AddGroupWithTop
 import Mathlib.Algebra.Order.AddTorsor
 import Mathlib.Algebra.Order.Algebra
 import Mathlib.Algebra.Order.Antidiag.Finsupp
@@ -546,7 +547,6 @@ import Mathlib.Algebra.Order.Group.Synonym
 import Mathlib.Algebra.Order.Group.TypeTags
 import Mathlib.Algebra.Order.Group.Unbundled.Basic
 import Mathlib.Algebra.Order.Group.Units
-import Mathlib.Algebra.Order.Group.WithTop
 import Mathlib.Algebra.Order.GroupWithZero.Canonical
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Support
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
-import Mathlib.Algebra.Order.Monoid.WithTop
+import Mathlib.Algebra.Order.AddGroupWithTop
 import Mathlib.Data.Nat.Cast.Field
 import Mathlib.Algebra.Field.Basic
 

Mathlib/Algebra/Order/AddGroupWithTop.lean

@@ -116,14 +116,6 @@ addition is monotone. -/
 class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, LinearOrder α
 #align linear_ordered_add_comm_group LinearOrderedAddCommGroup
 
-/-- A linearly ordered commutative group with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined. -/
-class LinearOrderedAddCommGroupWithTop (α : Type*) extends LinearOrderedAddCommMonoidWithTop α,
-  SubNegMonoid α, Nontrivial α where
-  protected neg_top : -(⊤ : α) = ⊤
-  protected add_neg_cancel : ∀ a : α, a ≠ ⊤ → a + -a = 0
-#align linear_ordered_add_comm_group_with_top LinearOrderedAddCommGroupWithTop
-
 /-- A linearly ordered commutative group is a
 commutative group with a linear order in which
 multiplication is monotone. -/

Mathlib/Algebra/Order/Group/Defs.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.GroupWithZero.WithZero
 import Mathlib.Algebra.Order.Group.Units
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.Order.Monoid.Basic
+import Mathlib.Algebra.Order.AddGroupWithTop
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.TypeTags
 import Mathlib.Algebra.Order.ZeroLEOne

Mathlib/Algebra/Order/Group/WithTop.lean

@@ -4,7 +4,6 @@ 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.Monoid.Unbundled.Basic
-import Mathlib.Order.BoundedOrder
 
 #align_import algebra.order.monoid.defs from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
 
@@ -137,31 +136,6 @@ class LinearOrderedCancelCommMonoid (α : Type*) extends OrderedCancelCommMonoid
 
 attribute [to_additive existing] LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid
 
-/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined. -/
-class LinearOrderedAddCommMonoidWithTop (α : Type*) extends LinearOrderedAddCommMonoid α,
-    OrderTop α where
-  /-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is invariant under addition. -/
-  protected top_add' : ∀ x : α, ⊤ + x = ⊤
-#align linear_ordered_add_comm_monoid_with_top LinearOrderedAddCommMonoidWithTop
-#align linear_ordered_add_comm_monoid_with_top.to_order_top LinearOrderedAddCommMonoidWithTop.toOrderTop
-
-section LinearOrderedAddCommMonoidWithTop
-
-variable [LinearOrderedAddCommMonoidWithTop α] {a b : α}
-
-@[simp]
-theorem top_add (a : α) : ⊤ + a = ⊤ :=
-  LinearOrderedAddCommMonoidWithTop.top_add' a
-#align top_add top_add
-
-@[simp]
-theorem add_top (a : α) : a + ⊤ = ⊤ :=
-  Trans.trans (add_comm _ _) (top_add _)
-#align add_top add_top
-
-end LinearOrderedAddCommMonoidWithTop
-
 variable [LinearOrderedCommMonoid α] {a : α}
 
 @[to_additive (attr := simp)]