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

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

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

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 = 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

  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 : 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 = 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.

class OrderedRing (α : Type u) extends Ring , PartialOrder : 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 = 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.

class OrderedCommRing (α : Type u) extends OrderedRing : 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 = 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.

class StrictOrderedSemiring (α : Type u) extends Semiring , PartialOrder , 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 = 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

  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 : 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 = 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.

class StrictOrderedRing (α : Type u) extends Ring , PartialOrder , 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 = 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.

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

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

class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring , Min , Max , Ord : 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 = 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 =.

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

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

class LinearOrderedRing (α : Type u) extends StrictOrderedRing , Min , Max , Ord : 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 = 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 =.

class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing : 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 = 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.

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

Equations

• (_ : ZeroLEOneClass α) = (_ : ZeroLEOneClass α)

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

Equations

• (_ : PosMulMono α) = (_ : CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x x_1 : α) => x ≤ x_1)

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

Equations

• (_ : MulPosMono α) = (_ : CovariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x x_1 : α) => x ≤ x_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 pow_le_pow_of_le_one {α : Type u} [OrderedSemiring α] {a : α} (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) {m : ℕ} {n : ℕ} : m ≤ n → a ^ n ≤ a ^ m

theorem pow_le_of_le_one {α : Type u} [OrderedSemiring α] {a : α} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a

theorem sq_le {α : Type u} [OrderedSemiring α] {a : α} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a

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

theorem mul_le_mul_of_nonpos_left {α : Type u} [OrderedSemiring α] {a : α} {b : α} {c : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b

theorem mul_le_mul_of_nonpos_right {α : Type u} [OrderedSemiring α] {a : α} {b : α} {c : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [OrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem mul_le_mul_of_nonneg_of_nonpos {α : Type u} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (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} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (ha : a ≤ 0) : Antitone fun (x : α) => a * x

theorem antitone_mul_right {α : Type u} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (ha : a ≤ 0) : Antitone fun (x : α) => x * a

theorem Monotone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [OrderedSemiring α] {a : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] {a : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] {a : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] {a : α} [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [Preorder β] {f : β → α} (hf : Antitone f) (ha : a ≤ 0) : Monotone fun (x : β) => f x * a

theorem Antitone.mul_monotone {α : Type u} {β : Type u_1} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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} [OrderedSemiring α] [ExistsAddOfLE α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ≤ b ↔ ∃ (c : α), c ≥ 0 ∧ b = a + c

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

Equations

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

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

• (_ : PosMulStrictMono α) = (_ : CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => ↑x * y) fun (x x_1 : α) => x < x_1)

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

Equations

• (_ : MulPosStrictMono α) = (_ : CovariantClass { x : α // 0 < x } α (fun (x : { x : α // 0 < x }) (y : α) => y * ↑x) fun (x x_1 : α) => x < x_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

• (_ : NoMaxOrder α) = (_ : NoMaxOrder α)

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

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

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

theorem lt_mul_of_lt_one_left {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] (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} [StrictOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] (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} [StrictOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] (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} [StrictOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] (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} [StrictOrderedSemiring α] [ExistsAddOfLE α] {a : α} (ha : a < 0) : StrictAnti fun (x : α) => a * x

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

theorem StrictMono.const_mul_of_neg {α : Type u} {β : Type u_1} [StrictOrderedSemiring α] {a : α} [ExistsAddOfLE α] [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} [StrictOrderedSemiring α] {a : α} [ExistsAddOfLE α] [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} [StrictOrderedSemiring α] {a : α} [ExistsAddOfLE α] [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} [StrictOrderedSemiring α] {a : α} [ExistsAddOfLE α] [Preorder β] {f : β → α} (hf : StrictAnti f) (ha : a < 0) : StrictMono fun (x : β) => f x * a

theorem mul_add_mul_le_mul_add_mul {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d

Binary rearrangement inequality.

theorem mul_add_mul_le_mul_add_mul' {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] (hba : b ≤ a) (hdc : d ≤ c) : a * d + b * c ≤ a * c + b * d

Binary rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d

Binary strict rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul' {α : Type u} [StrictOrderedSemiring α] {a : α} {b : α} {c : α} {d : α} [ExistsAddOfLE α] (hba : b < a) (hdc : d < c) : a * d + b * c < a * c + b * d

Binary rearrangement inequality.

@[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)

@[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

• (_ : PosMulReflectLT α) = (_ : ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => ↑x * y) fun (x x_1 : α) => x < x_1)

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

Equations

• (_ : MulPosReflectLT α) = (_ : ContravariantClass { x : α // 0 ≤ x } α (fun (x : { x : α // 0 ≤ x }) (y : α) => y * ↑x) fun (x x_1 : α) => x < x_1)

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg {α : 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 mul_nonneg_iff_of_pos_left {α : Type u} [LinearOrderedSemiring α] {b : α} {c : α} (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b

@[simp]

theorem mul_nonneg_iff_of_pos_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

theorem sign_cases_of_C_mul_pow_nonneg {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} (h : ∀ (n : ℕ), 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b

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

Equations

• (_ : NoZeroDivisors α) = (_ : NoZeroDivisors α)

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

Equations

• (_ : IsDomain α) = (_ : IsDomain α)

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

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

theorem mul_nonneg_of_three {α : Type u} [LinearOrderedSemiring α] [ExistsAddOfLE α] (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_nonneg_iff_pos_imp_nonneg {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] : 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem sq_nonneg {α : Type u} [LinearOrderedSemiring α] [ExistsAddOfLE α] (a : α) : 0 ≤ a ^ 2

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

theorem mul_self_add_mul_self_eq_zero {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] : a * a + b * b = 0 ↔ a = 0 ∧ b = 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} [LinearOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] (h : a * a + b * b = 0) : a = 0

theorem add_sq_le {α : Type u} [LinearOrderedSemiring α] {a : α} {b : α} [ExistsAddOfLE α] : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

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

Equations

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

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

theorem two_mul_le_add_sq {α : Type u} [LinearOrderedCommSemiring α] [ExistsAddOfLE α] (a : α) (b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2

Binary arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

theorem two_mul_le_add_pow_two {α : Type u} [LinearOrderedCommSemiring α] [ExistsAddOfLE α] (a : α) (b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2

Alias of two_mul_le_add_sq.

---

Binary arithmetic mean-geometric mean inequality (aka AM-GM inequality) for linearly ordered commutative semirings.

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.

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

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

theorem mul_nonneg_iff_neg_imp_nonpos {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

theorem mul_nonpos_iff_pos_imp_nonpos {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

theorem mul_nonpos_iff_neg_imp_nonneg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} : a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

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

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

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

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.

Deprecated lemmas

Those lemmas have been deprecated on 2023/12/23

@[deprecated mul_nonneg_iff_of_pos_left]

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

Alias of mul_nonneg_iff_of_pos_left.

@[deprecated mul_nonneg_iff_of_pos_right]

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

Alias of mul_nonneg_iff_of_pos_right.

@[deprecated mul_pos_iff_of_pos_left]

theorem zero_lt_mul_left {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (h : 0 < a) : 0 < a * b ↔ 0 < b

Alias of mul_pos_iff_of_pos_left.

@[deprecated mul_pos_iff_of_pos_right]

theorem zero_lt_mul_right {α : Type u_1} {a : α} {b : α} [MulZeroClass α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) : 0 < a * b ↔ 0 < a

Alias of mul_pos_iff_of_pos_right.