doc-next-gen

Mathlib.Algebra.Order.Ring.Defs

Module docstring

{"# 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 ","Note that OrderDual does not satisfy any of the ordered ring typeclasses due to the zero_le_one field. "}
IsOrderedRing structure
(R : Type*) [Semiring R] [PartialOrder R] extends IsOrderedAddMonoid R, ZeroLEOneClass R
Full source 
/-- An ordered semiring is a semiring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone. -/
class IsOrderedRing (R : Type*) [Semiring R] [PartialOrder R] extends
    IsOrderedAddMonoid R, ZeroLEOneClass R where
  /-- 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`. -/
  protected 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 right
  by a non-negative element `0 ≤ c` to obtain `a * c ≤ b * c`. -/
  protected mul_le_mul_of_nonneg_right : ∀ a b c : R, a ≤ b → 0 ≤ c → a * c ≤ b * c
Ordered Semiring
Informal description
An ordered semiring is a semiring $R$ equipped with a partial order $\leq$ such that: 1. Addition is monotone (if $a \leq b$ then $a + c \leq b + c$ for all $c$) 2. Multiplication by nonnegative elements is monotone (if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$) 3. The zero element is less than or equal to the one element ($0 \leq 1$)
IsStrictOrderedRing structure
(R : Type*) [Semiring R] [PartialOrder R] extends IsOrderedCancelAddMonoid R, ZeroLEOneClass R, Nontrivial R
Full source 
/-- 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. -/
class IsStrictOrderedRing (R : Type*) [Semiring R] [PartialOrder R] extends
    IsOrderedCancelAddMonoid R, ZeroLEOneClass R, Nontrivial R where
  /-- 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`. -/
  protected 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 right
  by a positive element `0 < c` to obtain `a * c < b * c`. -/
  protected mul_lt_mul_of_pos_right : ∀ a b c : R, a < b → 0 < c → a * c < b * c
Strict Ordered Semiring
Informal description
A strict ordered semiring is a nontrivial semiring with a partial order such that addition is strictly monotone (i.e., $a < b$ implies $a + c < b + c$ for all $c$) and multiplication by a positive number is strictly monotone (i.e., $0 < a$ and $b < c$ implies $a * b < a * c$). It also satisfies the condition that $0 \leq 1$.
IsOrderedRing.of_mul_nonneg theorem
[Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] (mul_nonneg : ∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) : IsOrderedRing R
Full source 
lemma IsOrderedRing.of_mul_nonneg [Ring R] [PartialOrder R] [IsOrderedAddMonoid R]
    [ZeroLEOneClass R] (mul_nonneg : ∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) :
    IsOrderedRing R where
  mul_le_mul_of_nonneg_left a b c ab hc := by
    simpa only [mul_sub, sub_nonneg] using mul_nonneg _ _ hc (sub_nonneg.2 ab)
  mul_le_mul_of_nonneg_right a b c ab hc := by
    simpa only [sub_mul, sub_nonneg] using mul_nonneg _ _ (sub_nonneg.2 ab) hc
Characterization of Ordered Rings via Nonnegative Multiplication
Informal description
Let $R$ be a ring with a partial order $\leq$ such that: 1. Addition is monotone (i.e., $R$ is an ordered additive monoid) 2. $0 \leq 1$ holds 3. Multiplication preserves nonnegativity (i.e., for all $a, b \in R$, if $0 \leq a$ and $0 \leq b$ then $0 \leq a \cdot b$) Then $R$ is an ordered ring, meaning multiplication by nonnegative elements is monotone (if $0 \leq a$ and $b \leq c$ then $a \cdot b \leq a \cdot c$).
IsStrictOrderedRing.of_mul_pos theorem
[Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R] (mul_pos : ∀ a b : R, 0 < a → 0 < b → 0 < a * b) : IsStrictOrderedRing R
Full source 
lemma IsStrictOrderedRing.of_mul_pos [Ring R] [PartialOrder R] [IsOrderedAddMonoid R]
    [ZeroLEOneClass R] [Nontrivial R] (mul_pos : ∀ a b : R, 0 < a → 0 < b → 0 < a * b) :
    IsStrictOrderedRing R where
  mul_lt_mul_of_pos_left a b c ab hc := by
    simpa only [mul_sub, sub_pos] using mul_pos _ _ hc (sub_pos.2 ab)
  mul_lt_mul_of_pos_right a b c ab hc := by
    simpa only [sub_mul, sub_pos] using mul_pos _ _ (sub_pos.2 ab) hc
Characterization of Strict Ordered Rings via Positive Multiplication
Informal description
Let $R$ be a ring equipped with a partial order $\leq$ such that: 1. Addition is monotone (i.e., $R$ is an ordered additive monoid) 2. $0 \leq 1$ holds 3. $R$ is nontrivial (i.e., $0 \neq 1$) 4. Multiplication preserves positivity (i.e., for all $a, b \in R$, if $0 < a$ and $0 < b$ then $0 < a \cdot b$) Then $R$ is a strict ordered ring, meaning: - Addition is strictly monotone (if $a < b$ then $a + c < b + c$ for all $c$) - Multiplication by positive elements is strictly monotone (if $0 < a$ and $b < c$ then $a \cdot b < a \cdot c$)
IsOrderedRing.toPosMulMono instance
: PosMulMono R
Full source 
instance (priority := 200) IsOrderedRing.toPosMulMono : PosMulMono R where
  elim x _ _ h := IsOrderedRing.mul_le_mul_of_nonneg_left _ _ _ h x.2
Monotonicity of Left Multiplication in Ordered Semirings
Informal description
For any ordered semiring $R$, left multiplication by nonnegative elements is monotone. That is, for any nonnegative element $b \in R$ and any elements $a_1, a_2 \in R$, if $a_1 \leq a_2$, then $b \cdot a_1 \leq b \cdot a_2$.
IsOrderedRing.toMulPosMono instance
: MulPosMono R
Full source 
instance (priority := 200) IsOrderedRing.toMulPosMono : MulPosMono R where
  elim x _ _ h := IsOrderedRing.mul_le_mul_of_nonneg_right _ _ _ h x.2
Monotonicity of Right Multiplication in Ordered Semirings
Informal description
For any ordered semiring $R$, right multiplication by nonnegative elements is monotone. That is, for any nonnegative element $b \in R$ and any elements $a_1, a_2 \in R$, if $a_1 \leq a_2$, then $a_1 \cdot b \leq a_2 \cdot b$.
IsOrderedRing.toIsStrictOrderedRing theorem
(R : Type*) [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R] : IsStrictOrderedRing R
Full source 
/-- Turn an ordered domain into a strict ordered ring. -/
lemma IsOrderedRing.toIsStrictOrderedRing (R : Type*)
    [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] [Nontrivial R] :
    IsStrictOrderedRing R :=
  .of_mul_pos fun _ _ ap bp ↦ (mul_nonneg ap.le bp.le).lt_of_ne' (mul_ne_zero ap.ne' bp.ne')
Characterization of Strict Ordered Rings via Ordered Rings with No Zero Divisors
Informal description
Let $R$ be a ring equipped with a partial order $\leq$ such that: 1. $R$ is an ordered ring (addition is monotone and multiplication by nonnegative elements is monotone) 2. $R$ has no zero divisors 3. $R$ is nontrivial (i.e., $0 \neq 1$) Then $R$ is a strict ordered ring, meaning: - Addition is strictly monotone (if $a < b$ then $a + c < b + c$ for all $c$) - Multiplication by positive elements is strictly monotone (if $0 < a$ and $b < c$ then $a \cdot b < a \cdot c$)
IsStrictOrderedRing.toPosMulStrictMono instance
: PosMulStrictMono R
Full source 
instance (priority := 200) IsStrictOrderedRing.toPosMulStrictMono : PosMulStrictMono R where
  elim x _ _ h := IsStrictOrderedRing.mul_lt_mul_of_pos_left _ _ _ h x.prop
Strict Monotonicity of Left Multiplication by Positive Elements in Strict Ordered Semirings
Informal description
In a strict ordered semiring $R$, left multiplication by a positive element is strictly monotone. That is, for any positive element $a > 0$ in $R$, if $b < c$, then $a \cdot b < a \cdot c$.
IsStrictOrderedRing.toMulPosStrictMono instance
: MulPosStrictMono R
Full source 
instance (priority := 200) IsStrictOrderedRing.toMulPosStrictMono : MulPosStrictMono R where
  elim x _ _ h := IsStrictOrderedRing.mul_lt_mul_of_pos_right _ _ _ h x.prop
Strict Monotonicity of Right Multiplication by Positive Elements in Strict Ordered Semirings
Informal description
In a strict ordered semiring $R$, right multiplication by a positive element is strictly monotone. That is, for any positive element $b > 0$ in $R$, if $a_1 < a_2$, then $a_1 * b < a_2 * b$.
IsStrictOrderedRing.noZeroDivisors instance
: NoZeroDivisors R
Full source 
instance (priority := 100) IsStrictOrderedRing.noZeroDivisors : NoZeroDivisors R where
  eq_zero_or_eq_zero_of_mul_eq_zero {a b} hab := by
    contrapose! hab
    obtain ha | ha := hab.1.lt_or_lt <;> obtain hb | hb := hab.2.lt_or_lt
    exacts [(mul_pos_of_neg_of_neg ha hb).ne', (mul_neg_of_neg_of_pos ha hb).ne,
      (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne']
Strict Ordered Semirings Have No Zero Divisors
Informal description
Every strict ordered semiring $R$ has no zero divisors, meaning that for any $a, b \in R$, if $a \cdot b = 0$, then either $a = 0$ or $b = 0$.
IsStrictOrderedRing.isDomain instance
: IsDomain R
Full source 
instance (priority := 100) IsStrictOrderedRing.isDomain : IsDomain R where
  mul_left_cancel_of_ne_zero {a b c} ha h := by
    obtain ha | ha := ha.lt_or_lt
    exacts [(strictAnti_mul_left ha).injective h, (strictMono_mul_left_of_pos ha).injective h]
  mul_right_cancel_of_ne_zero {b a c} ha h := by
    obtain ha | ha := ha.lt_or_lt
    exacts [(strictAnti_mul_right ha).injective h, (strictMono_mul_right_of_pos ha).injective h]
Strict Ordered Semirings are Domains
Informal description
Every strict ordered semiring $R$ is a domain, meaning it is a nontrivial semiring with no zero divisors.
OrderedSemiring structure
(R : Type u) extends Semiring R, OrderedAddCommMonoid R
Full source 
/-- An `OrderedSemiring` is a semiring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone. -/
@[deprecated "Use `[Semiring R] [PartialOrder R] [IsOrderedRing R]` instead."
  (since := "2025-04-10")]
structure OrderedSemiring (R : Type u) extends Semiring R, OrderedAddCommMonoid R where
  /-- `0 ≤ 1` in any ordered semiring. -/
  protected zero_le_one : (0 : R) ≤ 1
  /-- 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`. -/
  protected 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 right
  by a non-negative element `0 ≤ c` to obtain `a * c ≤ b * c`. -/
  protected mul_le_mul_of_nonneg_right : ∀ a b c : R, a ≤ b → 0 ≤ c → a * c ≤ b * c
Ordered Semiring
Informal description
An ordered semiring is a semiring $R$ equipped with a partial order such that addition is monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ for all $a, b, c \in R$) and multiplication by a nonnegative element is monotone (i.e., $0 \leq c$ and $a \leq b$ implies $a \cdot c \leq b \cdot c$ for all $a, b, c \in R$).
OrderedCommSemiring structure
(R : Type u) extends OrderedSemiring R, CommSemiring R
Full source 
/-- An `OrderedCommSemiring` is a commutative semiring with a partial order such that addition is
monotone and multiplication by a nonnegative number is monotone. -/
@[deprecated "Use `[CommSemiring R] [PartialOrder R] [IsOrderedRing R]` instead."
  (since := "2025-04-10")]
structure OrderedCommSemiring (R : Type u) extends OrderedSemiring R, CommSemiring R where
  mul_le_mul_of_nonneg_right a b c ha hc :=
    -- parentheses ensure this generates an `optParam` rather than an `autoParam`
    (by simpa only [mul_comm] using mul_le_mul_of_nonneg_left a b c ha hc)
Ordered Commutative Semiring
Informal description
An ordered commutative semiring is a commutative semiring \( R \) equipped with a partial order such that addition is monotone (i.e., \( a \leq b \) implies \( a + c \leq b + c \) for all \( c \)) and multiplication by a nonnegative element is monotone (i.e., \( 0 \leq c \) and \( a \leq b \) imply \( a \cdot c \leq b \cdot c \)).
OrderedRing structure
(R : Type u) extends Ring R, OrderedAddCommGroup R
Full source 
/-- An `OrderedRing` is a ring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone. -/
@[deprecated "Use `[Ring R] [PartialOrder R] [IsOrderedRing R]` instead."
  (since := "2025-04-10")]
structure OrderedRing (R : Type u) extends Ring R, OrderedAddCommGroup R where
  /-- `0 ≤ 1` in any ordered ring. -/
  protected zero_le_one : 0 ≤ (1 : R)
  /-- The product of non-negative elements is non-negative. -/
  protected mul_nonneg : ∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
Ordered Ring
Informal description
An ordered ring is a ring equipped with a partial order such that addition is monotone (i.e., respects the order) and multiplication by a nonnegative element is monotone (i.e., preserves the order when multiplying by nonnegative elements).
OrderedCommRing structure
(R : Type u) extends OrderedRing R, CommRing R
Full source 
/-- An `OrderedCommRing` is a commutative ring with a partial order such that addition is monotone
and multiplication by a nonnegative number is monotone. -/
@[deprecated "Use `[CommRing R] [PartialOrder R] [IsOrderedRing R]` instead."
  (since := "2025-04-10")]
structure OrderedCommRing (R : Type u) extends OrderedRing R, CommRing R
Ordered Commutative Ring
Informal description
An ordered commutative ring is a commutative ring $R$ equipped with a partial order such that addition is monotone (preserves the order) and multiplication by nonnegative elements is monotone. This means: 1. For any $a, b, c \in R$, if $a \leq b$ then $a + c \leq b + c$. 2. For any $a, b \in R$ and $c \geq 0$, if $a \leq b$ then $a \cdot c \leq b \cdot c$.
StrictOrderedSemiring structure
(R : Type u) extends Semiring R, OrderedCancelAddCommMonoid R, Nontrivial R
Full source 
/-- 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. -/
@[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 where
  /-- In a strict ordered semiring, `0 ≤ 1`. -/
  protected zero_le_one : (0 : R) ≤ 1
  /-- Left multiplication by a positive element is strictly monotone. -/
  protected mul_lt_mul_of_pos_left : ∀ a b c : R, a < b → 0 < c → c * a < c * b
  /-- Right multiplication by a positive element is strictly monotone. -/
  protected mul_lt_mul_of_pos_right : ∀ a b c : R, a < b → 0 < c → a * c < b * c
Strictly Ordered Semiring
Informal description
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.
StrictOrderedCommSemiring structure
(R : Type u) extends StrictOrderedSemiring R, CommSemiring R
Full source 
/-- 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. -/
@[deprecated "Use `[CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure StrictOrderedCommSemiring (R : Type u) extends StrictOrderedSemiring R, CommSemiring R
Strictly Ordered Commutative Semiring
Informal description
A `StrictOrderedCommSemiring` is a commutative semiring with a partial order where addition is strictly monotone (i.e., preserves `<`) and multiplication by a positive number is strictly monotone. This structure combines the properties of a commutative semiring with those of an ordered additive commutative monoid where the order interacts strictly with both addition and multiplication.
StrictOrderedRing structure
(R : Type u) extends Ring R, OrderedAddCommGroup R, Nontrivial R
Full source 
/-- A `StrictOrderedRing` is a ring with a partial order such that addition is strictly monotone
and multiplication by a positive number is strictly monotone. -/
@[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 where
  /-- In a strict ordered ring, `0 ≤ 1`. -/
  protected zero_le_one : 0 ≤ (1 : R)
  /-- The product of two positive elements is positive. -/
  protected mul_pos : ∀ a b : R, 0 < a → 0 < b → 0 < a * b
Strictly Ordered Ring
Informal description
A `StrictOrderedRing` is a ring $R$ equipped with a partial order such that addition is strictly monotone (i.e., $a < b$ implies $a + c < b + c$ for all $c$) and multiplication by a positive element is strictly monotone (i.e., $0 < c$ and $a < b$ implies $a * c < b * c$). Additionally, the ring is required to be nontrivial (i.e., it contains at least two distinct elements).
StrictOrderedCommRing structure
(R : Type*) extends StrictOrderedRing R, CommRing R
Full source 
/-- 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. -/
@[deprecated "Use `[CommRing R] [PartialOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure StrictOrderedCommRing (R : Type*) extends StrictOrderedRing R, CommRing R
Strictly Ordered Commutative Ring
Informal description
A `StrictOrderedCommRing` is a commutative ring $R$ equipped with a partial order such that: 1. Addition is strictly monotone: for any $a, b, c \in R$, if $a < b$ then $a + c < b + c$. 2. Multiplication by a positive element is strictly monotone: for any $a, b, c \in R$, if $a < b$ and $0 < c$ then $a * c < b * c$. 3. The ring is nontrivial (i.e., $0 \neq 1$).
LinearOrderedSemiring structure
(R : Type u) extends StrictOrderedSemiring R, LinearOrderedAddCommMonoid R
Full source 
/-- A `LinearOrderedSemiring` is a nontrivial semiring with a linear order such that
addition is monotone and multiplication by a positive number is strictly monotone. -/
@[deprecated "Use `[Semiring R] [LinearOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure LinearOrderedSemiring (R : Type u) extends StrictOrderedSemiring R,
  LinearOrderedAddCommMonoid R
Linearly Ordered Semiring
Informal description
A `LinearOrderedSemiring` is a structure consisting of a nontrivial semiring $R$ equipped with a linear order, where addition is monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ for all $c$) and multiplication by a positive element is strictly monotone (i.e., $a < b$ and $0 < c$ implies $a \cdot c < b \cdot c$).
LinearOrderedCommSemiring structure
(R : Type*) extends StrictOrderedCommSemiring R, LinearOrderedSemiring R
Full source 
/-- 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. -/
@[deprecated "Use `[CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCommSemiring (R : Type*) extends StrictOrderedCommSemiring R,
  LinearOrderedSemiring R
Linearly Ordered Commutative Semiring
Informal description
A linearly ordered commutative semiring is a nontrivial commutative semiring equipped with a linear order, where addition is monotone (preserves the order) and multiplication by a positive number is strictly monotone (strictly preserves the order).
LinearOrderedRing structure
(R : Type u) extends StrictOrderedRing R, LinearOrder R
Full source 
/-- A `LinearOrderedRing` is a ring with a linear order such that addition is monotone and
multiplication by a positive number is strictly monotone. -/
@[deprecated "Use `[Ring R] [LinearOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure LinearOrderedRing (R : Type u) extends StrictOrderedRing R, LinearOrder R
Linearly Ordered Ring
Informal description
A `LinearOrderedRing` is a ring $R$ equipped with a linear order such that addition is monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ for all $c$) and multiplication by a positive element is strictly monotone (i.e., $a < b$ and $0 < c$ implies $a \cdot c < b \cdot c$).
LinearOrderedCommRing structure
(R : Type u) extends LinearOrderedRing R, CommMonoid R
Full source 
/-- A `LinearOrderedCommRing` is a commutative ring with a linear order such that addition is
monotone and multiplication by a positive number is strictly monotone. -/
@[deprecated "Use `[CommRing R] [LinearOrder R] [IsStrictOrderedRing R]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCommRing (R : Type u) extends LinearOrderedRing R, CommMonoid R
Linearly Ordered Commutative Ring
Informal description
A `LinearOrderedCommRing` is a commutative ring \( R \) equipped with a linear order such that: 1. Addition is monotone: for any \( a, b, c \in R \), if \( a \leq b \), then \( a + c \leq b + c \). 2. Multiplication by a positive element is strictly monotone: for any \( a, b, c \in R \), if \( a < b \) and \( 0 < c \), then \( a * c < b * c \).
one_add_le_one_sub_mul_one_add theorem
(h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c)
Full source 
lemma one_add_le_one_sub_mul_one_add (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c) := by
  rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr
Inequality relating $(1 + a)$ and $(1 - b)(1 + c)$ in ordered semirings
Informal description
Let $a, b, c$ be elements of an ordered semiring $R$ such that $a + b + b \cdot c \leq c$. Then it follows that $1 + a \leq (1 - b) \cdot (1 + c)$.
one_add_le_one_add_mul_one_sub theorem
(h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c)
Full source 
lemma one_add_le_one_add_mul_one_sub (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c) := by
  rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr
Inequality $(1 + a) \leq (1 + b)(1 - c)$ in ordered semirings
Informal description
Let $R$ be an ordered semiring and let $a, b, c \in R$ satisfy $a + c + b \cdot c \leq b$. Then $1 + a \leq (1 + b) \cdot (1 - c)$.
one_sub_le_one_sub_mul_one_add theorem
(h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c)
Full source 
lemma one_sub_le_one_sub_mul_one_add (h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c) := by
  rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]
  gcongr
Inequality $(1 - a) \leq (1 - b)(1 + c)$ in ordered semirings
Informal description
Let $R$ be an ordered semiring and let $a, b, c \in R$ satisfy $b + b \cdot c \leq a + c$. Then $1 - a \leq (1 - b) \cdot (1 + c)$.
one_sub_le_one_add_mul_one_sub theorem
(h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c)
Full source 
lemma one_sub_le_one_add_mul_one_sub (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c) := by
  rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
  gcongr
Inequality $(1 - a) \leq (1 + b)(1 - c)$ in ordered semirings
Informal description
Let $R$ be an ordered semiring and let $a, b, c \in R$ satisfy $c + b \cdot c \leq a + b$. Then $1 - a \leq (1 + b) \cdot (1 - c)$.