Ordered rings and semirings

This file develops the basics of ordered (semi)rings.

Each typeclass here comprises

• an algebraic class (Semiring, CommSemiring, Ring, CommRing)
• an order class (PartialOrder, LinearOrder)
• assumptions on how both interact ((strict) monotonicity, canonicity)

For short,

• "+ respects ≤" means "monotonicity of addition"
• "+ respects <" means "strict monotonicity of addition"
• "* respects ≤" means "monotonicity of multiplication by a nonnegative number".
• "* respects <" means "strict monotonicity of multiplication by a positive number".

Typeclasses

• OrderedSemiring: Semiring with a partial order such that + and * respect ≤.
• StrictOrderedSemiring: Nontrivial semiring with a partial order such that + and * respects <.
• OrderedCommSemiring: Commutative semiring with a partial order such that + and * respect ≤.
• StrictOrderedCommSemiring: Nontrivial commutative semiring with a partial order such that + and * respect <.
• OrderedRing: Ring with a partial order such that + respects ≤ and * respects <.
• OrderedCommRing: Commutative ring with a partial order such that + respects ≤ and * respects <.
• LinearOrderedSemiring: Nontrivial semiring with a linear order such that + respects ≤ and * respects <.
• LinearOrderedCommSemiring: Nontrivial commutative semiring with a linear order such that + respects ≤ and * respects <.
• LinearOrderedRing: Nontrivial ring with a linear order such that + respects ≤ and * respects <.
• LinearOrderedCommRing: Nontrivial commutative ring with a linear order such that + respects ≤ and * respects <.

Hierarchy

The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.

• OrderedSemiring
  • OrderedAddCommMonoid & multiplication & * respects ≤
  • Semiring & partial order structure & + respects ≤ & * respects ≤
• StrictOrderedSemiring
  • OrderedCancelAddCommMonoid & multiplication & * respects < & nontriviality
  • OrderedSemiring & + respects < & * respects < & nontriviality
• OrderedCommSemiring
  • OrderedSemiring & commutativity of multiplication
  • CommSemiring & partial order structure & + respects ≤ & * respects <
• StrictOrderedCommSemiring
  • StrictOrderedSemiring & commutativity of multiplication
  • OrderedCommSemiring & + respects < & * respects < & nontriviality
• OrderedRing
  • OrderedSemiring & additive inverses
  • OrderedAddCommGroup & multiplication & * respects <
  • Ring & partial order structure & + respects ≤ & * respects <
• StrictOrderedRing
  • StrictOrderedSemiring & additive inverses
  • OrderedSemiring & + respects < & * respects < & nontriviality
• OrderedCommRing
  • OrderedRing & commutativity of multiplication
  • OrderedCommSemiring & additive inverses
  • CommRing & partial order structure & + respects ≤ & * respects <
• StrictOrderedCommRing
  • StrictOrderedCommSemiring & additive inverses
  • StrictOrderedRing & commutativity of multiplication
  • OrderedCommRing & + respects < & * respects < & nontriviality
• LinearOrderedSemiring
  • StrictOrderedSemiring & totality of the order
  • LinearOrderedAddCommMonoid & multiplication & nontriviality & * respects <
• LinearOrderedCommSemiring
  • StrictOrderedCommSemiring & totality of the order
  • LinearOrderedSemiring & commutativity of multiplication
• LinearOrderedRing
  • StrictOrderedRing & totality of the order
  • LinearOrderedSemiring & additive inverses
  • LinearOrderedAddCommGroup & multiplication & * respects <
  • Ring & IsDomain & linear order structure
• LinearOrderedCommRing
  • StrictOrderedCommRing & totality of the order
  • LinearOrderedRing & commutativity of multiplication
  • LinearOrderedCommSemiring & additive inverses
  • CommRing & IsDomain & linear order structure

class IsOrderedRing (R : Type u_1) [Semiring R] [PartialOrder R] extends IsOrderedAddMonoid R, ZeroLEOneClass R : Prop

An ordered semiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• zero_le_one : 0 ≤ 1
• mul_le_mul_of_nonneg_left (a b c : R) : a ≤ b → 0 ≤ c → c * a ≤ c * b

  In an ordered semiring, we can multiply an inequality a ≤ b on the left by a non-negative element 0 ≤ c to obtain c * a ≤ c * b.

• mul_le_mul_of_nonneg_right (a b c : R) : a ≤ b → 0 ≤ c → a * c ≤ b * c

  In an ordered semiring, we can multiply an inequality a ≤ b on the right by a non-negative element 0 ≤ c to obtain a * c ≤ b * c.

class IsStrictOrderedRing (R : Type u_1) [Semiring R] [PartialOrder R] extends IsOrderedCancelAddMonoid R, ZeroLEOneClass R, Nontrivial R : Prop

A strict ordered semiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• add_le_add_right (a b : R) : a ≤ b → ∀ (c : R), a + c ≤ b + c
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• le_of_add_le_add_right (a b c : R) : b + a ≤ c + a → b ≤ c
• zero_le_one : 0 ≤ 1
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• mul_lt_mul_of_pos_left (a b c : R) : a < b → 0 < c → c * a < c * b

  In a strict ordered semiring, we can multiply an inequality a < b on the left by a positive element 0 < c to obtain c * a < c * b.

• mul_lt_mul_of_pos_right (a b c : R) : a < b → 0 < c → a * c < b * c

  In a strict ordered semiring, we can multiply an inequality a < b on the right by a positive element 0 < c to obtain a * c < b * c.

instance instOrderedRingOfIsStrictOrderedRing {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Lean.Grind.OrderedRing R

theorem IsOrderedRing.of_mul_nonneg {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] (mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b) : IsOrderedRing R

theorem IsStrictOrderedRing.of_mul_pos {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R] (mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b) : IsStrictOrderedRing R

@[instance 200]

instance IsOrderedRing.toPosMulMono {R : Type u} [Semiring R] [PartialOrder R] [IsOrderedRing R] : PosMulMono R

@[instance 200]

instance IsOrderedRing.toMulPosMono {R : Type u} [Semiring R] [PartialOrder R] [IsOrderedRing R] : MulPosMono R

@[instance 50]

instance IsOrderedRing.toIsStrictOrderedRing (R : Type u_1) [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R] : IsStrictOrderedRing R

Turn an ordered domain into a strict ordered ring.

@[instance 200]

instance IsStrictOrderedRing.toPosMulStrictMono {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : PosMulStrictMono R

@[instance 200]

instance IsStrictOrderedRing.toMulPosStrictMono {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulPosStrictMono R

@[instance 100]

instance IsStrictOrderedRing.toIsOrderedRing {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsOrderedRing R

theorem AddMonoidWithOne.toCharZero {R : Type u_1} [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] : CharZero R

This is not an instance, as it would loop with NeZero.charZero_one.

@[instance 100]

instance IsStrictOrderedRing.toCharZero {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : CharZero R

@[instance 100]

instance IsStrictOrderedRing.toNoMaxOrder {R : Type u} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : NoMaxOrder R

@[instance 100]

instance IsStrictOrderedRing.noZeroDivisors {R : Type u} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : NoZeroDivisors R

@[instance 100]

instance IsStrictOrderedRing.isDomain {R : Type u} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] : IsDomain R

Note that OrderDual does not satisfy any of the ordered ring typeclasses due to the zero_le_one field.

@[deprecated "Use `[Semiring R] [PartialOrder R] [IsOrderedRing R]` instead." (since := "2025-04-10")]

structure OrderedSemiring (R : Type u) extends Semiring R, OrderedAddCommMonoid R : Type u

An OrderedSemiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• zero_le_one : 0 ≤ 1

  0 ≤ 1 in any ordered semiring.

• mul_le_mul_of_nonneg_left (a b c : R) : a ≤ b → 0 ≤ c → c * a ≤ c * b

  In an ordered semiring, we can multiply an inequality a ≤ b on the left by a non-negative element 0 ≤ c to obtain c * a ≤ c * b.

• mul_le_mul_of_nonneg_right (a b c : R) : a ≤ b → 0 ≤ c → a * c ≤ b * c

  In an ordered semiring, we can multiply an inequality a ≤ b on the right by a non-negative element 0 ≤ c to obtain a * c ≤ b * c.

@[deprecated "Use `[CommSemiring R] [PartialOrder R] [IsOrderedRing R]` instead." (since := "2025-04-10")]

structure OrderedCommSemiring (R : Type u) extends OrderedSemiring R, CommSemiring R : Type u

An OrderedCommSemiring is a commutative semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• zero_le_one : 0 ≤ 1
• mul_le_mul_of_nonneg_left (a b c : R) : a ≤ b → 0 ≤ c → c * a ≤ c * b
• mul_le_mul_of_nonneg_right (a b c : R) : a ≤ b → 0 ≤ c → a * c ≤ b * c
• mul_comm (a b : R) : a * b = b * a

@[deprecated "Use `[Ring R] [PartialOrder R] [IsOrderedRing R]` instead." (since := "2025-04-10")]

structure OrderedRing (R : Type u) extends Ring R, OrderedAddCommGroup R : Type u

An OrderedRing is a ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• zero_le_one : 0 ≤ 1

  0 ≤ 1 in any ordered ring.

• mul_nonneg (a b : R) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b

  The product of non-negative elements is non-negative.

@[deprecated "Use `[CommRing R] [PartialOrder R] [IsOrderedRing R]` instead." (since := "2025-04-10")]

structure OrderedCommRing (R : Type u) extends OrderedRing R, CommRing R : Type u

An OrderedCommRing is a commutative ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• zero_le_one : 0 ≤ 1
• mul_nonneg (a b : R) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b
• mul_comm (a b : R) : a * b = b * a

@[deprecated "Use `[Semiring R] [PartialOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure StrictOrderedSemiring (R : Type u) extends Semiring R, OrderedCancelAddCommMonoid R, Nontrivial R : Type u

A StrictOrderedSemiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1

  In a strict ordered semiring, 0 ≤ 1.

• mul_lt_mul_of_pos_left (a b c : R) : a < b → 0 < c → c * a < c * b

  Left multiplication by a positive element is strictly monotone.

• mul_lt_mul_of_pos_right (a b c : R) : a < b → 0 < c → a * c < b * c

  Right multiplication by a positive element is strictly monotone.

@[deprecated "Use `[CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure StrictOrderedCommSemiring (R : Type u) extends StrictOrderedSemiring R, CommSemiring R : Type u

A StrictOrderedCommSemiring is a commutative semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : R) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : R) : a < b → 0 < c → a * c < b * c
• mul_comm (a b : R) : a * b = b * a

@[deprecated "Use `[Ring R] [PartialOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure StrictOrderedRing (R : Type u) extends Ring R, OrderedAddCommGroup R, Nontrivial R : Type u

A StrictOrderedRing is a ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1

  In a strict ordered ring, 0 ≤ 1.

• mul_pos (a b : R) : 0 < a → 0 < b → 0 < a * b

  The product of two positive elements is positive.

@[deprecated "Use `[CommRing R] [PartialOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure StrictOrderedCommRing (R : Type u_1) extends StrictOrderedRing R, CommRing R : Type u_1

A StrictOrderedCommRing is a commutative ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos (a b : R) : 0 < a → 0 < b → 0 < a * b
• mul_comm (a b : R) : a * b = b * a

@[deprecated "Use `[Semiring R] [LinearOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure LinearOrderedSemiring (R : Type u) extends StrictOrderedSemiring R, LinearOrderedAddCommMonoid R : Type u

A LinearOrderedSemiring is a nontrivial semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : R) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : R) : a < b → 0 < c → a * c < b * c
• min : R → R → R
• max : R → R → R
• compare : R → R → Ordering
• le_total (a b : R) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE R
• toDecidableEq : DecidableEq R
• toDecidableLT : DecidableLT R
• min_def (a b : R) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : R) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : R) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure LinearOrderedCommSemiring (R : Type u_1) extends StrictOrderedCommSemiring R, LinearOrderedSemiring R : Type u_1

A LinearOrderedCommSemiring is a nontrivial commutative semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• le_of_add_le_add_left (a b c : R) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : R) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : R) : a < b → 0 < c → a * c < b * c
• mul_comm (a b : R) : a * b = b * a
• min : R → R → R
• max : R → R → R
• compare : R → R → Ordering
• le_total (a b : R) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE R
• toDecidableEq : DecidableEq R
• toDecidableLT : DecidableLT R
• min_def (a b : R) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : R) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : R) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[Ring R] [LinearOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure LinearOrderedRing (R : Type u) extends StrictOrderedRing R, LinearOrder R : Type u

A LinearOrderedRing is a ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos (a b : R) : 0 < a → 0 < b → 0 < a * b
• min : R → R → R
• max : R → R → R
• compare : R → R → Ordering
• le_total (a b : R) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE R
• toDecidableEq : DecidableEq R
• toDecidableLT : DecidableLT R
• min_def (a b : R) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : R) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : R) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[CommRing R] [LinearOrder R] [IsStrictOrderedRing R]` instead." (since := "2025-04-10")]

structure LinearOrderedCommRing (R : Type u) extends LinearOrderedRing R, CommMonoid R : Type u

A LinearOrderedCommRing is a commutative ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : R) : a + b = b + a
• mul : R → R → R
• left_distrib (a b c : R) : a * (b + c) = a * b + a * c
• right_distrib (a b c : R) : (a + b) * c = a * c + b * c
• zero_mul (a : R) : 0 * a = 0
• mul_zero (a : R) : a * 0 = 0
• mul_assoc (a b c : R) : a * b * c = a * (b * c)
• one : R
• one_mul (a : R) : 1 * a = a
• mul_one (a : R) : a * 1 = a
• natCast : ℕ → R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → R → R
• npow_zero (x : R) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : R) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg (a b : R) : a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' (a : R) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : R) : -a + a = 0
• intCast : ℤ → R
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : R → R → Prop
• lt : R → R → Prop
• le_refl (a : R) : a ≤ a
• le_trans (a b c : R) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : R) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : R) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : R) : a ≤ b → ∀ (c : R), c + a ≤ c + b
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos (a b : R) : 0 < a → 0 < b → 0 < a * b
• min : R → R → R
• max : R → R → R
• compare : R → R → Ordering
• le_total (a b : R) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE R
• toDecidableEq : DecidableEq R
• toDecidableLT : DecidableLT R
• min_def (a b : R) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : R) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : R) : compare a b = compareOfLessAndEq a b
• mul_comm (a b : R) : a * b = b * a

theorem one_add_le_one_sub_mul_one_add {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c)

theorem one_add_le_one_add_mul_one_sub {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c)

theorem one_sub_le_one_sub_mul_one_add {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c)

theorem one_sub_le_one_add_mul_one_sub {R : Type u} [Ring R] [PartialOrder R] [IsOrderedRing R] {a b c : R} (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c)