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 <.
• CanonicallyOrderedCommSemiring: Commutative semiring with a partial order such that + respects ≤, * respects <, and a ≤ b ↔ ∃ c, b = a + c.

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 <
  • Domain & linear order structure
• LinearOrderedCommRing
  • StrictOrderedCommRing & totality of the order
  • LinearOrderedRing & commutativity of multiplication
  • LinearOrderedCommSemiring & additive inverses
  • IsDomain & linear order structure

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

theorem add_one_le_two_mul {α : Type u} [LE α] [Semiring α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a

class OrderedSemiring (α : Type u) extends Semiring , PartialOrder : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  Addition is monotone in an OrderedAddCommMonoid.

• 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.

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

class OrderedCommSemiring (α : Type u) extends OrderedSemiring : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  Multiplication is commutative in a commutative semigroup.

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

class OrderedRing (α : Type u) extends Ring , PartialOrder : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  Addition is monotone in an ordered additive commutative group.

• 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.

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

class OrderedCommRing (α : Type u) extends OrderedRing : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  Multiplication is commutative in a commutative semigroup.

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

class StrictOrderedSemiring (α : Type u) extends Semiring , PartialOrder , Nontrivial : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  Addition is monotone in an ordered cancellative additive commutative monoid.

• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c

  Additive cancellation is compatible with the order in an ordered cancellative additive commutative monoid.

• 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.

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.

class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  Multiplication is commutative in a commutative semigroup.

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.

class StrictOrderedRing (α : Type u) extends Ring , PartialOrder , Nontrivial : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  Addition is monotone in an ordered additive commutative group.

• 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.

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

class StrictOrderedCommRing (α : Type u_2) extends StrictOrderedRing : Type u_2

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  Multiplication is commutative in a commutative semigroup.

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.

class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring , Min , Max , Ord : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq α

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b

  The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a

  The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

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

class LinearOrderedCommSemiring (α : Type u_2) extends StrictOrderedCommSemiring , Min , Max , Ord : Type u_2

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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

  A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq α

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b

  The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a

  The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

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.

class LinearOrderedRing (α : Type u) extends StrictOrderedRing , Min , Max , Ord : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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

  A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq α

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b

  The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a

  The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

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

class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing : Type u

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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 : DecidableRel fun x x_1 => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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

  Multiplication is commutative in a commutative semigroup.

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

instance OrderedSemiring.zeroLEOneClass {α : Type u} [OrderedSemiring α] : ZeroLEOneClass α

Equations

• @OrderedSemiring.zeroLEOneClass = @OrderedSemiring.zeroLEOneClass.proof_1

instance OrderedSemiring.toPosMulMono {α : Type u} [OrderedSemiring α] : PosMulMono α

Equations

• @OrderedSemiring.toPosMulMono = @OrderedSemiring.toPosMulMono.proof_1

instance OrderedSemiring.toMulPosMono {α : Type u} [OrderedSemiring α] : MulPosMono α

Equations

• @OrderedSemiring.toMulPosMono = @OrderedSemiring.toMulPosMono.proof_1

theorem bit1_mono {α : Type u} [OrderedSemiring α] : Monotone bit1

@[simp]

theorem pow_nonneg {α : Type u} [OrderedSemiring α] {a : α} (H : 0 ≤ a) (n : ℕ) : 0 ≤ a ^ n

theorem add_le_mul_two_add {α : Type u} [OrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b)

theorem one_le_mul_of_one_le_of_one_le {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

theorem monotone_mul_left_of_nonneg {α : Type u} [OrderedSemiring α] {a : α} (ha : 0 ≤ a) : Monotone fun x => a * x

theorem monotone_mul_right_of_nonneg {α : Type u} [OrderedSemiring α] {a : α} (ha : 0 ≤ a) : Monotone fun x => x * a

theorem Monotone.mul_const {α : Type u} {β : Type u_1} [OrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x => f x * a

theorem Monotone.const_mul {α : Type u} {β : Type u_1} [OrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : Monotone f) (ha : 0 ≤ a) : Monotone fun x => a * f x

theorem Antitone.mul_const {α : Type u} {β : Type u_1} [OrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x => f x * a

theorem Antitone.const_mul {α : Type u} {β : Type u_1} [OrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : Antitone f) (ha : 0 ≤ a) : Antitone fun x => a * f x

theorem Monotone.mul {α : Type u} {β : Type u_1} [OrderedSemiring α] [Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : Monotone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : Monotone (f * g)

theorem bit1_pos {α : Type u} [OrderedSemiring α] {a : α} [Nontrivial α] (h : 0 ≤ a) : 0 < bit1 a

theorem bit1_pos' {α : Type u} [OrderedSemiring α] {a : α} (h : 0 < a) : 0 < bit1 a

theorem mul_le_one {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) : a * b ≤ 1

theorem one_lt_mul_of_le_of_lt {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

theorem one_lt_mul_of_lt_of_le {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

theorem one_lt_mul {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Alias of one_lt_mul_of_le_of_lt.

theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha₀ : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) : a * b < 1

theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [OrderedSemiring α] {a : α} {b : α} (ha : a ≤ 1) (hb₀ : 0 ≤ b) (hb : b < 1) : a * b < 1

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

Equations

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

theorem mul_le_mul_of_nonpos_left {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b

theorem mul_le_mul_of_nonpos_right {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [OrderedRing α] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem mul_le_mul_of_nonneg_of_nonpos {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d

theorem mul_le_mul_of_nonneg_of_nonpos' {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

theorem mul_le_mul_of_nonpos_of_nonneg {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d

theorem mul_le_mul_of_nonpos_of_nonneg' {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

theorem mul_le_mul_of_nonpos_of_nonpos {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hdb : d ≤ b) (hc : c ≤ 0) (hb : b ≤ 0) : a * b ≤ c * d

theorem mul_le_mul_of_nonpos_of_nonpos' {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} {d : α} (hca : c ≤ a) (hdb : d ≤ b) (ha : a ≤ 0) (hd : d ≤ 0) : a * b ≤ c * d

theorem le_mul_of_le_one_left {α : Type u} [OrderedRing α] {a : α} {b : α} (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b

Variant of mul_le_of_le_one_left for b non-positive instead of non-negative.

theorem mul_le_of_one_le_left {α : Type u} [OrderedRing α] {a : α} {b : α} (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b

Variant of le_mul_of_one_le_left for b non-positive instead of non-negative.

theorem le_mul_of_le_one_right {α : Type u} [OrderedRing α] {a : α} {b : α} (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b

Variant of mul_le_of_le_one_right for a non-positive instead of non-negative.

theorem mul_le_of_one_le_right {α : Type u} [OrderedRing α] {a : α} {b : α} (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a

Variant of le_mul_of_one_le_right for a non-positive instead of non-negative.

theorem antitone_mul_left {α : Type u} [OrderedRing α] {a : α} (ha : a ≤ 0) : Antitone ((fun x x_1 => x * x_1) a)

theorem antitone_mul_right {α : Type u} [OrderedRing α] {a : α} (ha : a ≤ 0) : Antitone fun x => x * a

theorem Monotone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [OrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => a * f x

theorem Monotone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [OrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => f x * a

theorem Antitone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [OrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => a * f x

theorem Antitone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [OrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => f x * a

theorem Antitone.mul_monotone {α : Type u} {β : Type u_1} [OrderedRing α] [Preorder β] {f : β → α} {g : β → α} (hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ (x : β), f x ≤ 0) (hg₀ : ∀ (x : β), 0 ≤ g x) : Antitone (f * g)

theorem Monotone.mul_antitone {α : Type u} {β : Type u_1} [OrderedRing α] [Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), g x ≤ 0) : Antitone (f * g)

theorem Antitone.mul {α : Type u} {β : Type u_1} [OrderedRing α] [Preorder β] {f : β → α} {g : β → α} (hf : Antitone f) (hg : Antitone g) (hf₀ : ∀ (x : β), f x ≤ 0) (hg₀ : ∀ (x : β), g x ≤ 0) : Monotone (f * g)

theorem le_iff_exists_nonneg_add {α : Type u} [OrderedRing α] (a : α) (b : α) : a ≤ b ↔ ∃ c, c ≥ 0 ∧ b = a + c

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

Equations

• OrderedCommRing.toOrderedCommSemiring = let src := OrderedRing.toOrderedSemiring; let src_1 := inst; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

instance StrictOrderedSemiring.toPosMulStrictMono {α : Type u} [StrictOrderedSemiring α] : PosMulStrictMono α

Equations

• @StrictOrderedSemiring.toPosMulStrictMono = @StrictOrderedSemiring.toPosMulStrictMono.proof_1

instance StrictOrderedSemiring.toMulPosStrictMono {α : Type u} [StrictOrderedSemiring α] : MulPosStrictMono α

Equations

• @StrictOrderedSemiring.toMulPosStrictMono = @StrictOrderedSemiring.toMulPosStrictMono.proof_1

@[reducible]

def StrictOrderedSemiring.toOrderedSemiring' {α : Type u} [StrictOrderedSemiring α] [DecidableRel fun x x_1 => x ≤ x_1] : 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 StrictOrderedSemiring.toOrderedSemiring {α : Type u} [StrictOrderedSemiring α] : OrderedSemiring α

Equations

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

theorem mul_lt_mul {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) (hc : 0 ≤ c) : a * b < c * d

theorem mul_lt_mul' {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b < d) (hb : 0 ≤ b) (hc : 0 < c) : a * b < c * d

@[simp]

theorem pow_pos {α : Type u} [StrictOrderedSemiring α] {a : α} (H : 0 < a) (n : ℕ) : 0 < a ^ n

theorem mul_self_lt_mul_self {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b

theorem strictMonoOn_mul_self {α : Type u} [StrictOrderedSemiring α] : StrictMonoOn (fun x => x * x) {x | 0 ≤ x}

theorem Decidable.mul_lt_mul'' {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [DecidableRel fun x x_1 => x ≤ x_1] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d

theorem mul_lt_mul'' {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d

theorem lt_mul_left {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} (hn : 0 < a) (hm : 1 < b) : a < b * a

theorem lt_mul_right {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} (hn : 0 < a) (hm : 1 < b) : a < a * b

theorem lt_mul_self {α : Type u} [StrictOrderedSemiring α] {a : α} (hn : 1 < a) : a < a * a

theorem strictMono_mul_left_of_pos {α : Type u} [StrictOrderedSemiring α] {a : α} (ha : 0 < a) : StrictMono fun x => a * x

theorem strictMono_mul_right_of_pos {α : Type u} [StrictOrderedSemiring α] {a : α} (ha : 0 < a) : StrictMono fun x => x * a

theorem StrictMono.mul_const {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x => f x * a

theorem StrictMono.const_mul {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : StrictMono f) (ha : 0 < a) : StrictMono fun x => a * f x

theorem StrictAnti.mul_const {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x => f x * a

theorem StrictAnti.const_mul {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] {a : α} [Preorder β] {f : β → α} (hf : StrictAnti f) (ha : 0 < a) : StrictAnti fun x => a * f x

theorem StrictMono.mul_monotone {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] [Preorder β] {f : β → α} {g : β → α} (hf : StrictMono f) (hg : Monotone g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 < g x) : StrictMono (f * g)

theorem Monotone.mul_strictMono {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] [Preorder β] {f : β → α} {g : β → α} (hf : Monotone f) (hg : StrictMono g) (hf₀ : ∀ (x : β), 0 < f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : StrictMono (f * g)

theorem StrictMono.mul {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] [Preorder β] {f : β → α} {g : β → α} (hf : StrictMono f) (hg : StrictMono g) (hf₀ : ∀ (x : β), 0 ≤ f x) (hg₀ : ∀ (x : β), 0 ≤ g x) : StrictMono (f * g)

theorem lt_two_mul_self {α : Type u} [StrictOrderedSemiring α] {a : α} (ha : 0 < a) : a < 2 * a

instance StrictOrderedSemiring.toNoMaxOrder {α : Type u} [StrictOrderedSemiring α] : NoMaxOrder α

Equations

• @StrictOrderedSemiring.toNoMaxOrder = @StrictOrderedSemiring.toNoMaxOrder.proof_1

@[reducible]

def StrictOrderedCommSemiring.toOrderedCommSemiring' {α : Type u} [StrictOrderedCommSemiring α] [DecidableRel fun x x_1 => x ≤ x_1] : OrderedCommSemiring α

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

Equations

• StrictOrderedCommSemiring.toOrderedCommSemiring' = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring'; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• StrictOrderedCommSemiring.toOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedSemiring.toOrderedSemiring; OrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

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

@[reducible]

def StrictOrderedRing.toOrderedRing' {α : Type u} [StrictOrderedRing α] [DecidableRel fun x x_1 => x ≤ x_1] : OrderedRing α

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

Equations

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

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

Equations

• StrictOrderedRing.toOrderedRing = let src := inst; OrderedRing.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) (_ : 0 ≤ 1) (_ : ∀ (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

theorem mul_lt_mul_of_neg_left {α : Type u} [StrictOrderedRing α] {a : α} {b : α} {c : α} (h : b < a) (hc : c < 0) : c * a < c * b

theorem mul_lt_mul_of_neg_right {α : Type u} [StrictOrderedRing α] {a : α} {b : α} {c : α} (h : b < a) (hc : c < 0) : a * c < b * c

theorem mul_pos_of_neg_of_neg {α : Type u} [StrictOrderedRing α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b

theorem lt_mul_of_lt_one_left {α : Type u} [StrictOrderedRing α] {a : α} {b : α} (hb : b < 0) (h : a < 1) : b < a * b

Variant of mul_lt_of_lt_one_left for b negative instead of positive.

theorem mul_lt_of_one_lt_left {α : Type u} [StrictOrderedRing α] {a : α} {b : α} (hb : b < 0) (h : 1 < a) : a * b < b

Variant of lt_mul_of_one_lt_left for b negative instead of positive.

theorem lt_mul_of_lt_one_right {α : Type u} [StrictOrderedRing α] {a : α} {b : α} (ha : a < 0) (h : b < 1) : a < a * b

Variant of mul_lt_of_lt_one_right for a negative instead of positive.

theorem mul_lt_of_one_lt_right {α : Type u} [StrictOrderedRing α] {a : α} {b : α} (ha : a < 0) (h : 1 < b) : a * b < a

Variant of lt_mul_of_lt_one_right for a negative instead of positive.

theorem strictAnti_mul_left {α : Type u} [StrictOrderedRing α] {a : α} (ha : a < 0) : StrictAnti ((fun x x_1 => x * x_1) a)

theorem strictAnti_mul_right {α : Type u} [StrictOrderedRing α] {a : α} (ha : a < 0) : StrictAnti fun x => x * a

theorem StrictMono.const_mul_of_neg {α : Type u} {β : Type u_1} [StrictOrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => a * f x

theorem StrictMono.mul_const_of_neg {α : Type u} {β : Type u_1} [StrictOrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => f x * a

theorem StrictAnti.const_mul_of_neg {α : Type u} {β : Type u_1} [StrictOrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => a * f x

theorem StrictAnti.mul_const_of_neg {α : Type u} {β : Type u_1} [StrictOrderedRing α] {a : α} [Preorder β] {f : β → α} (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => f x * a

@[reducible]

def StrictOrderedCommRing.toOrderedCommRing' {α : Type u} [StrictOrderedCommRing α] [DecidableRel fun x x_1 => x ≤ x_1] : OrderedCommRing α

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

Equations

• StrictOrderedCommRing.toOrderedCommRing' = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing'; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• StrictOrderedCommRing.toStrictOrderedCommSemiring = let src := inst; let src_1 := StrictOrderedRing.toStrictOrderedSemiring; StrictOrderedCommSemiring.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

• StrictOrderedCommRing.toOrderedCommRing = let src := inst; let src_1 := StrictOrderedRing.toOrderedRing; OrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

instance LinearOrderedSemiring.toPosMulReflectLT {α : Type u} [LinearOrderedSemiring α] : PosMulReflectLT α

Equations

• @LinearOrderedSemiring.toPosMulReflectLT = @LinearOrderedSemiring.toPosMulReflectLT.proof_1

instance LinearOrderedSemiring.toMulPosReflectLT {α : Type u} [LinearOrderedSemiring α] : MulPosReflectLT α

Equations

• @LinearOrderedSemiring.toMulPosReflectLT = @LinearOrderedSemiring.toMulPosReflectLT.proof_1

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (hab : 0 ≤ a * b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem nonneg_of_mul_nonneg_left {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a

theorem nonneg_of_mul_nonneg_right {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b

theorem neg_of_mul_neg_left {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : a * b < 0) (hb : 0 ≤ b) : a < 0

theorem neg_of_mul_neg_right {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : a * b < 0) (ha : 0 ≤ a) : b < 0

theorem nonpos_of_mul_nonpos_left {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0

theorem nonpos_of_mul_nonpos_right {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0

@[simp]

theorem zero_le_mul_left {α : Type u} [LinearOrderedSemiring α] {b : α} {c : α} (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b

@[simp]

theorem zero_le_mul_right {α : Type u} [LinearOrderedSemiring α] {b : α} {c : α} (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b

theorem add_le_mul_of_left_le_right {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b

theorem add_le_mul_of_right_le_left {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b

theorem add_le_mul {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b

theorem add_le_mul' {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ b * a

@[simp]

theorem bit0_le_bit0 {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} : bit0 a ≤ bit0 b ↔ a ≤ b

@[simp]

theorem bit0_lt_bit0 {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} : bit0 a < bit0 b ↔ a < b

@[simp]

theorem bit1_le_bit1 {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} : bit1 a ≤ bit1 b ↔ a ≤ b

@[simp]

theorem bit1_lt_bit1 {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} : bit1 a < bit1 b ↔ a < b

@[simp]

theorem one_le_bit1 {α : Type u} [LinearOrderedSemiring α] {a : α} : 1 ≤ bit1 a ↔ 0 ≤ a

@[simp]

theorem one_lt_bit1 {α : Type u} [LinearOrderedSemiring α] {a : α} : 1 < bit1 a ↔ 0 < a

@[simp]

theorem zero_le_bit0 {α : Type u} [LinearOrderedSemiring α] {a : α} : 0 ≤ bit0 a ↔ 0 ≤ a

@[simp]

theorem zero_lt_bit0 {α : Type u} [LinearOrderedSemiring α] {a : α} : 0 < bit0 a ↔ 0 < a

theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (ha : 0 < a) : 0 ≤ a * b ↔ 0 ≤ b

theorem mul_nonneg_iff_left_nonneg_of_pos {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

theorem nonpos_of_mul_nonneg_left {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0

theorem nonpos_of_mul_nonneg_right {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0

@[simp]

theorem Units.inv_pos {α : Type u} [LinearOrderedSemiring α] {u : αˣ} : 0 < ↑u⁻¹ ↔ 0 < ↑u

@[simp]

theorem Units.inv_neg {α : Type u} [LinearOrderedSemiring α] {u : αˣ} : ↑u⁻¹ < 0 ↔ ↑u < 0

theorem cmp_mul_pos_left {α : Type u} [LinearOrderedSemiring α] {a : α} (ha : 0 < a) (b : α) (c : α) : cmp (a * b) (a * c) = cmp b c

theorem cmp_mul_pos_right {α : Type u} [LinearOrderedSemiring α] {a : α} (ha : 0 < a) (b : α) (c : α) : cmp (b * a) (c * a) = cmp b c

theorem mul_max_of_nonneg {α : Type u} [LinearOrderedSemiring α] {a : α} (b : α) (c : α) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c)

theorem mul_min_of_nonneg {α : Type u} [LinearOrderedSemiring α] {a : α} (b : α) (c : α) (ha : 0 ≤ a) : a * min b c = min (a * b) (a * c)

theorem max_mul_of_nonneg {α : Type u} [LinearOrderedSemiring α] {c : α} (a : α) (b : α) (hc : 0 ≤ c) : max a b * c = max (a * c) (b * c)

theorem min_mul_of_nonneg {α : Type u} [LinearOrderedSemiring α] {c : α} (a : α) (b : α) (hc : 0 ≤ c) : min a b * c = min (a * c) (b * c)

theorem le_of_mul_le_of_one_le {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} {c : α} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) : a ≤ b

theorem nonneg_le_nonneg_of_sq_le_sq {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (hb : 0 ≤ b) (h : a * a ≤ b * b) : a ≤ b

theorem mul_self_le_mul_self_iff {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a ≤ b ↔ a * a ≤ b * b

theorem mul_self_lt_mul_self_iff {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b

theorem mul_self_inj {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b

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

Equations

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

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

Equations

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

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

Equations

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

instance LinearOrderedRing.noZeroDivisors {α : Type u} [LinearOrderedRing α] : NoZeroDivisors α

Equations

• @LinearOrderedRing.noZeroDivisors = @LinearOrderedRing.noZeroDivisors.proof_1

instance LinearOrderedRing.isDomain {α : Type u} [LinearOrderedRing α] : IsDomain α

Equations

• @LinearOrderedRing.isDomain = @LinearOrderedRing.isDomain.proof_1

theorem mul_pos_iff {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem mul_neg_iff {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

theorem mul_nonneg_iff {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem mul_nonneg_of_three {α : Type u} [LinearOrderedRing α] (a : α) (b : α) (c : α) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Out of three elements of a LinearOrderedRing, two must have the same sign.

theorem mul_nonpos_iff {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem mul_self_nonneg {α : Type u} [LinearOrderedRing α] (a : α) : 0 ≤ a * a

@[simp]

theorem neg_le_self_iff {α : Type u} [LinearOrderedRing α] {a : α} : -a ≤ a ↔ 0 ≤ a

@[simp]

theorem neg_lt_self_iff {α : Type u} [LinearOrderedRing α] {a : α} : -a < a ↔ 0 < a

@[simp]

theorem le_neg_self_iff {α : Type u} [LinearOrderedRing α] {a : α} : a ≤ -a ↔ a ≤ 0

@[simp]

theorem lt_neg_self_iff {α : Type u} [LinearOrderedRing α] {a : α} : a < -a ↔ a < 0

theorem neg_one_lt_zero {α : Type u} [LinearOrderedRing α] : -1 < 0

@[simp]

theorem mul_le_mul_left_of_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a

@[simp]

theorem mul_le_mul_right_of_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a

@[simp]

theorem mul_lt_mul_left_of_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : c * a < c * b ↔ b < a

@[simp]

theorem mul_lt_mul_right_of_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c < 0) : a * c < b * c ↔ b < a

theorem lt_of_mul_lt_mul_of_nonpos_left {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : c * a < c * b) (hc : c ≤ 0) : b < a

theorem lt_of_mul_lt_mul_of_nonpos_right {α : Type u} [LinearOrderedRing α] {a : α} {b : α} {c : α} (h : a * c < b * c) (hc : c ≤ 0) : b < a

theorem cmp_mul_neg_left {α : Type u} [LinearOrderedRing α] {a : α} (ha : a < 0) (b : α) (c : α) : cmp (a * b) (a * c) = cmp c b

theorem cmp_mul_neg_right {α : Type u} [LinearOrderedRing α] {a : α} (ha : a < 0) (b : α) (c : α) : cmp (b * a) (c * a) = cmp c b

theorem sub_one_lt {α : Type u} [LinearOrderedRing α] (a : α) : a - 1 < a

@[simp]

theorem mul_self_pos {α : Type u} [LinearOrderedRing α] {a : α} : 0 < a * a ↔ a ≠ 0

theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} [LinearOrderedRing α] {x : α} {y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) : x * x ≤ y * y

theorem nonneg_of_mul_nonpos_left {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a

theorem nonneg_of_mul_nonpos_right {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b

theorem pos_of_mul_neg_left {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (h : a * b < 0) (hb : b ≤ 0) : 0 < a

theorem pos_of_mul_neg_right {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (h : a * b < 0) (ha : a ≤ 0) : 0 < b

theorem neg_iff_pos_of_mul_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (hab : a * b < 0) : a < 0 ↔ 0 < b

theorem pos_iff_neg_of_mul_neg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (hab : a * b < 0) : 0 < a ↔ b < 0

theorem mul_self_add_mul_self_eq_zero {α : Type u} [LinearOrderedRing α] {x : α} {y : α} : x * x + y * y = 0 ↔ x = 0 ∧ y = 0

The sum of two squares is zero iff both elements are zero.

theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [LinearOrderedRing α] {a : α} {b : α} (h : a * a + b * b = 0) : a = 0

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

Equations

• LinearOrderedCommRing.toStrictOrderedCommRing = StrictOrderedCommRing.mk (_ : ∀ (a b : α), a * b = b * a)

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

Equations

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

theorem max_mul_mul_le_max_mul_max {α : Type u} [LinearOrderedCommRing α] {a : α} {d : α} (b : α) (c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) : max (a * b) (d * c) ≤ max a c * max d b