fix

Mathlib/Algebra/Order/Pi.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Ring.Pi
 

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -4,17 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Ring.Unbundled.Basic
--- import Mathlib.Algebra.CharZero.Defs
--- import Mathlib.Algebra.Group.Pi.Basic
--- import Mathlib.Algebra.Group.Units
--- import Mathlib.Algebra.GroupWithZero.NeZero
+import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Algebra.Order.Group.Defs
--- import Mathlib.Algebra.Order.GroupWithZero.Unbundled
--- import Mathlib.Algebra.Order.Monoid.Canonical.Defs
--- import Mathlib.Algebra.Order.Monoid.NatCast
--- import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
--- import Mathlib.Algebra.Ring.Defs
--- import Mathlib.Tactic.Tauto
 
 #align_import algebra.order.ring.char_zero from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"
 #align_import algebra.order.ring.defs from "leanprover-community/mathlib"@"44e29dbcff83ba7114a464d592b8c3743987c1e5"
@@ -306,6 +297,11 @@ instance (priority := 100) StrictOrderedSemiring.toCharZero [StrictOrderedSemiri
     (strictMono_nat_of_lt_succ fun n ↦ by rw [Nat.cast_succ]; apply lt_add_one).injective
 #align strict_ordered_semiring.to_char_zero StrictOrderedSemiring.toCharZero
 
+-- see Note [lower instance priority]
+instance (priority := 100) StrictOrderedSemiring.toNoMaxOrder : NoMaxOrder α :=
+  ⟨fun a => ⟨a + 1, lt_add_of_pos_right _ one_pos⟩⟩
+#align strict_ordered_semiring.to_no_max_order StrictOrderedSemiring.toNoMaxOrder
+
 end StrictOrderedSemiring
 
 section StrictOrderedCommSemiring

Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

@@ -3,13 +3,12 @@ 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, Yaël Dillies
 -/
-import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Algebra.Group.Units
 import Mathlib.Algebra.GroupWithZero.NeZero
-import Mathlib.Algebra.Order.Group.Defs
+import Mathlib.Algebra.Order.Group.Unbundled.Basic
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Algebra.Order.Monoid.NatCast
 import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Algebra.Ring.Defs
@@ -19,11 +18,12 @@ import Mathlib.Tactic.Tauto
 #align_import algebra.order.ring.defs from "leanprover-community/mathlib"@"44e29dbcff83ba7114a464d592b8c3743987c1e5"
 
 /-!
-# Ordered rings and semirings
+# Basic facts for ordered rings and semirings
 
-This file develops the basics of ordered (semi)rings.
+This file develops the basics of ordered (semi)rings in an unbundled fashion for later use with
+the bundled classes from `Algebra.Order.Ring.Defs`.
 
-Each typeclass here comprises
+The set of typeclass variables here comprises
 * an algebraic class (`Semiring`, `CommSemiring`, `Ring`, `CommRing`)
 * an order class (`PartialOrder`, `LinearOrder`)
 * assumptions on how both interact ((strict) monotonicity, canonicity)
@@ -34,7 +34,7 @@ For short,
 * "`*` respects `≤`" means "monotonicity of multiplication by a nonnegative number".
 * "`*` respects `<`" means "strict monotonicity of multiplication by a positive number".
 
-## Typeclasses
+## Typeclasses found in `Algebra.Order.Ring.Defs`
 
 * `OrderedSemiring`: Semiring with a partial order such that `+` and `*` respect `≤`.
 * `StrictOrderedSemiring`: Nontrivial semiring with a partial order such that `+` and `*` respects
@@ -106,8 +106,20 @@ immediate predecessors and what conditions are added to each of them.
   - `LinearOrderedRing` & commutativity of multiplication
   - `LinearOrderedCommSemiring` & additive inverses
   - `CommRing` & `IsDomain` & linear order structure
+
+## Generality
+
+Each section is labelled with a corresponding bundled ordered ring typeclass in mind. Mixin's for
+relating the order structures and ring structures are added as needed.
+
+TODO: the mixin assumptiosn can be relaxed in most cases
+
 -/
 
+
+assert_not_exists OrderedCommMonoid
+assert_not_exists MonoidHom
+
 open Function
 
 universe u
@@ -983,4 +995,3 @@ end LinearOrderedRing
 @[deprecated (since := "2023-12-23")] alias zero_lt_mul_left := mul_pos_iff_of_pos_left
 @[deprecated (since := "2023-12-23")] alias zero_lt_mul_right := mul_pos_iff_of_pos_right
 
-assert_not_exists MonoidHom