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 (α : Type u_1) [Semiring α] [PartialOrder α] extends IsOrderedAddMonoid α, ZeroLEOneClass α : 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 : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• zero_le_one : 0 ≤ 1
• mul_le_mul_of_nonneg_left (a b c : α) : 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 : α) : 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 (α : Type u_1) [Semiring α] [PartialOrder α] extends IsOrderedCancelAddMonoid α, ZeroLEOneClass α, Nontrivial α : 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 : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• le_of_add_le_add_right (a b c : α) : b + a ≤ c + a → b ≤ c
• zero_le_one : 0 ≤ 1
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• mul_lt_mul_of_pos_left (a b c : α) : 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 : α) : 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.

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

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

@[instance 200]

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

@[instance 200]

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

theorem IsOrderedRing.toIsStrictOrderedRing (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] [NoZeroDivisors α] [Nontrivial α] : IsStrictOrderedRing α

Turn an ordered domain into a strict ordered ring.

@[instance 200]

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

@[instance 200]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

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

class OrderedSemiring (α : Type u) extends Semiring α, OrderedAddCommMonoid α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• zero_le_one : 0 ≤ 1

  0 ≤ 1 in any ordered semiring.

• mul_le_mul_of_nonneg_left (a b c : α) : 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 : α) : 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 OrderedCommSemiring (α : Type u) extends OrderedSemiring α, CommSemiring α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• zero_le_one : 0 ≤ 1
• mul_le_mul_of_nonneg_left (a b c : α) : a ≤ b → 0 ≤ c → c * a ≤ c * b
• mul_le_mul_of_nonneg_right (a b c : α) : a ≤ b → 0 ≤ c → a * c ≤ b * c
• mul_comm (a b : α) : a * b = b * a

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

  0 ≤ 1 in any ordered ring.

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

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

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

class StrictOrderedSemiring (α : Type u) extends Semiring α, OrderedCancelAddCommMonoid α, Nontrivial α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1

  In a strict ordered semiring, 0 ≤ 1.

• mul_lt_mul_of_pos_left (a b c : α) : 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 : α) : a < b → 0 < c → a * c < b * c

  Right multiplication by a positive element is strictly monotone.

class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring α, CommSemiring α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : α) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : α) : a < b → 0 < c → a * c < b * c
• mul_comm (a b : α) : a * b = b * a

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

  In a strict ordered ring, 0 ≤ 1.

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

  The product of two positive elements is positive.

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

class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring α, LinearOrderedAddCommMonoid α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : α) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : α) : a < b → 0 < c → a * c < b * c
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• decidableLE : DecidableLE α
• decidableEq : DecidableEq α
• decidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

class LinearOrderedCommSemiring (α : Type u_1) extends StrictOrderedCommSemiring α, LinearOrderedSemiring α : 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 : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : α) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : α) : a < b → 0 < c → a * c < b * c
• mul_comm (a b : α) : a * b = b * a
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• decidableLE : DecidableLE α
• decidableEq : DecidableEq α
• decidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

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

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

instance OrderedSemiring.toIsOrderedRing {α : Type u} [OrderedSemiring α] : IsOrderedRing α

@[instance 100]

instance OrderedRing.toOrderedSemiring {α : Type u} [OrderedRing α] : OrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

theorem one_add_le_one_sub_mul_one_add {α : Type u} [OrderedRing α] {a b c : α} (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c)

theorem one_add_le_one_add_mul_one_sub {α : Type u} [OrderedRing α] {a b c : α} (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c)

theorem one_sub_le_one_sub_mul_one_add {α : Type u} [OrderedRing α] {a b c : α} (h : b + b * c ≤ a + c) : 1 - a ≤ (1 - b) * (1 + c)

theorem one_sub_le_one_add_mul_one_sub {α : Type u} [OrderedRing α] {a b c : α} (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c)

@[instance 100]

instance OrderedCommRing.toOrderedCommSemiring {α : Type u} [OrderedCommRing α] : OrderedCommSemiring α

Equations

• OrderedCommRing.toOrderedCommSemiring = { toOrderedSemiring := OrderedRing.toOrderedSemiring, mul_comm := ⋯ }

instance StrictOrderedSemiring.toIsStrictOrderedRing {α : Type u} [StrictOrderedSemiring α] : IsStrictOrderedRing α

@[reducible, inline]

abbrev StrictOrderedSemiring.toOrderedSemiring' {α : Type u} [StrictOrderedSemiring α] [DecidableLE α] : OrderedSemiring α

A choice-free version of StrictOrderedSemiring.toOrderedSemiring to avoid using choice in basic Nat lemmas.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance StrictOrderedSemiring.toOrderedSemiring {α : Type u} [StrictOrderedSemiring α] : OrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev StrictOrderedCommSemiring.toOrderedCommSemiring' {α : Type u} [StrictOrderedCommSemiring α] [DecidableLE α] : OrderedCommSemiring α

A choice-free version of StrictOrderedCommSemiring.toOrderedCommSemiring' to avoid using choice in basic Nat lemmas.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance StrictOrderedCommSemiring.toOrderedCommSemiring {α : Type u} [StrictOrderedCommSemiring α] : OrderedCommSemiring α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance StrictOrderedRing.toStrictOrderedSemiring {α : Type u} [StrictOrderedRing α] : StrictOrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev StrictOrderedRing.toOrderedRing' {α : Type u} [StrictOrderedRing α] [DecidableLE α] : OrderedRing α

A choice-free version of StrictOrderedRing.toOrderedRing to avoid using choice in basic Int lemmas.

Equations

• StrictOrderedRing.toOrderedRing' = { toRing := StrictOrderedRing.toRing, toPartialOrder := StrictOrderedRing.toPartialOrder, add_le_add_left := ⋯, zero_le_one := ⋯, mul_nonneg := ⋯ }

@[instance 100]

instance StrictOrderedRing.toOrderedRing {α : Type u} [StrictOrderedRing α] : OrderedRing α

Equations

• StrictOrderedRing.toOrderedRing = { toRing := StrictOrderedRing.toRing, toPartialOrder := StrictOrderedRing.toPartialOrder, add_le_add_left := ⋯, zero_le_one := ⋯, mul_nonneg := ⋯ }

@[reducible, inline]

abbrev StrictOrderedCommRing.toOrderedCommRing' {α : Type u} [StrictOrderedCommRing α] [DecidableLE α] : OrderedCommRing α

A choice-free version of StrictOrderedCommRing.toOrderedCommRing to avoid using choice in basic Int lemmas.

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance StrictOrderedCommRing.toStrictOrderedCommSemiring {α : Type u} [StrictOrderedCommRing α] : StrictOrderedCommSemiring α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance StrictOrderedCommRing.toOrderedCommRing {α : Type u} [StrictOrderedCommRing α] : OrderedCommRing α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance LinearOrderedSemiring.toLinearOrderedCancelAddCommMonoid {α : Type u} [LinearOrderedSemiring α] : LinearOrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance LinearOrderedRing.toLinearOrderedSemiring {α : Type u} [LinearOrderedRing α] : LinearOrderedSemiring α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance LinearOrderedRing.toLinearOrderedAddCommGroup {α : Type u} [LinearOrderedRing α] : LinearOrderedAddCommGroup α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance LinearOrderedCommRing.toStrictOrderedCommRing {α : Type u} [d : LinearOrderedCommRing α] : StrictOrderedCommRing α

Equations

• LinearOrderedCommRing.toStrictOrderedCommRing = { toStrictOrderedRing := LinearOrderedRing.toStrictOrderedRing, mul_comm := ⋯ }

@[instance 100]

instance LinearOrderedCommRing.toLinearOrderedCommSemiring {α : Type u} [d : LinearOrderedCommRing α] : LinearOrderedCommSemiring α

Equations

• One or more equations did not get rendered due to their size.