Documentation

Mathlib.Algebra.Order.Ring.Defs

Ordered rings and semirings #

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

Each typeclass here comprises

For short,

Typeclasses #

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.

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 :

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

  • add : ααα
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : αα
  • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : ααα
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • natCast : α
  • natCast_zero : 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 = Semiring.npow n x * x
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = 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 b0 cc * 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 b0 ca * 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.

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

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

    • add : ααα
    • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
    • zero : α
    • zero_add : ∀ (a : α), 0 + a = a
    • add_zero : ∀ (a : α), a + 0 = a
    • nsmul : αα
    • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
    • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
    • add_comm : ∀ (a b : α), a + b = b + a
    • mul : ααα
    • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
    • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
    • zero_mul : ∀ (a : α), 0 * a = 0
    • mul_zero : ∀ (a : α), a * 0 = 0
    • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
    • one : α
    • one_mul : ∀ (a : α), 1 * a = a
    • mul_one : ∀ (a : α), a * 1 = a
    • natCast : α
    • natCast_zero : 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 = Semiring.npow n x * x
    • le : ααProp
    • lt : ααProp
    • le_refl : ∀ (a : α), a a
    • le_trans : ∀ (a b c : α), a bb ca c
    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
    • le_antisymm : ∀ (a b : α), a bb aa = 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 b0 cc * a c * b
    • mul_le_mul_of_nonneg_right : ∀ (a b c : α), a b0 ca * c b * c
    • mul_comm : ∀ (a b : α), a * b = b * a

      Multiplication is commutative in a commutative multiplicative magma.

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

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

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

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

        Instances

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

          • add : ααα
          • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
          • zero : α
          • zero_add : ∀ (a : α), 0 + a = a
          • add_zero : ∀ (a : α), a + 0 = a
          • nsmul : αα
          • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
          • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
          • add_comm : ∀ (a b : α), a + b = b + a
          • mul : ααα
          • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
          • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
          • zero_mul : ∀ (a : α), 0 * a = 0
          • mul_zero : ∀ (a : α), a * 0 = 0
          • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
          • one : α
          • one_mul : ∀ (a : α), 1 * a = a
          • mul_one : ∀ (a : α), a * 1 = a
          • natCast : α
          • natCast_zero : 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 = Semiring.npow n x * x
          • le : ααProp
          • lt : ααProp
          • le_refl : ∀ (a : α), a a
          • le_trans : ∀ (a b c : α), a bb ca c
          • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
          • le_antisymm : ∀ (a b : α), a bb aa = 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 + cb 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 < b0 < cc * a < c * b

            Left multiplication by a positive element is strictly monotone.

          • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c

            Right multiplication by a positive element is strictly monotone.

          Instances

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

            • add : ααα
            • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
            • zero : α
            • zero_add : ∀ (a : α), 0 + a = a
            • add_zero : ∀ (a : α), a + 0 = a
            • nsmul : αα
            • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
            • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
            • add_comm : ∀ (a b : α), a + b = b + a
            • mul : ααα
            • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
            • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
            • zero_mul : ∀ (a : α), 0 * a = 0
            • mul_zero : ∀ (a : α), a * 0 = 0
            • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
            • one : α
            • one_mul : ∀ (a : α), 1 * a = a
            • mul_one : ∀ (a : α), a * 1 = a
            • natCast : α
            • natCast_zero : 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 = Semiring.npow n x * x
            • le : ααProp
            • lt : ααProp
            • le_refl : ∀ (a : α), a a
            • le_trans : ∀ (a b c : α), a bb ca c
            • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
            • le_antisymm : ∀ (a b : α), a bb aa = 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 + cb c
            • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
            • zero_le_one : 0 1
            • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
            • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c
            • mul_comm : ∀ (a b : α), a * b = b * a

              Multiplication is commutative in a commutative multiplicative magma.

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

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

              • add : ααα
              • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
              • zero : α
              • zero_add : ∀ (a : α), 0 + a = a
              • add_zero : ∀ (a : α), a + 0 = a
              • nsmul : αα
              • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
              • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
              • add_comm : ∀ (a b : α), a + b = b + a
              • mul : ααα
              • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
              • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
              • zero_mul : ∀ (a : α), 0 * a = 0
              • mul_zero : ∀ (a : α), a * 0 = 0
              • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
              • one : α
              • one_mul : ∀ (a : α), 1 * a = a
              • mul_one : ∀ (a : α), a * 1 = a
              • natCast : α
              • natCast_zero : 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 = Semiring.npow n x * x
              • neg : αα
              • sub : ααα
              • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
              • zsmul : αα
              • zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
              • zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = Ring.zsmul (Int.ofNat n) a + 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 bb ca c
              • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
              • le_antisymm : ∀ (a b : α), a bb aa = 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 < a0 < b0 < a * b

                The product of two positive elements is positive.

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

                Instances

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

                  • add : ααα
                  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
                  • zero : α
                  • zero_add : ∀ (a : α), 0 + a = a
                  • add_zero : ∀ (a : α), a + 0 = a
                  • nsmul : αα
                  • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
                  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
                  • add_comm : ∀ (a b : α), a + b = b + a
                  • mul : ααα
                  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
                  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
                  • zero_mul : ∀ (a : α), 0 * a = 0
                  • mul_zero : ∀ (a : α), a * 0 = 0
                  • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
                  • one : α
                  • one_mul : ∀ (a : α), 1 * a = a
                  • mul_one : ∀ (a : α), a * 1 = a
                  • natCast : α
                  • natCast_zero : 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 = Semiring.npow n x * x
                  • le : ααProp
                  • lt : ααProp
                  • le_refl : ∀ (a : α), a a
                  • le_trans : ∀ (a b c : α), a bb ca c
                  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
                  • le_antisymm : ∀ (a b : α), a bb aa = 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 + cb c
                  • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
                  • zero_le_one : 0 1
                  • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
                  • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * 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 =.

                  Instances

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

                    • add : ααα
                    • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
                    • zero : α
                    • zero_add : ∀ (a : α), 0 + a = a
                    • add_zero : ∀ (a : α), a + 0 = a
                    • nsmul : αα
                    • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
                    • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
                    • add_comm : ∀ (a b : α), a + b = b + a
                    • mul : ααα
                    • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
                    • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
                    • zero_mul : ∀ (a : α), 0 * a = 0
                    • mul_zero : ∀ (a : α), a * 0 = 0
                    • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
                    • one : α
                    • one_mul : ∀ (a : α), 1 * a = a
                    • mul_one : ∀ (a : α), a * 1 = a
                    • natCast : α
                    • natCast_zero : 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 = Semiring.npow n x * x
                    • le : ααProp
                    • lt : ααProp
                    • le_refl : ∀ (a : α), a a
                    • le_trans : ∀ (a b c : α), a bb ca c
                    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
                    • le_antisymm : ∀ (a b : α), a bb aa = 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 + cb c
                    • exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
                    • zero_le_one : 0 1
                    • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
                    • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * 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 =.

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

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

                      • add : ααα
                      • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
                      • zero : α
                      • zero_add : ∀ (a : α), 0 + a = a
                      • add_zero : ∀ (a : α), a + 0 = a
                      • nsmul : αα
                      • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
                      • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
                      • add_comm : ∀ (a b : α), a + b = b + a
                      • mul : ααα
                      • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
                      • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
                      • zero_mul : ∀ (a : α), 0 * a = 0
                      • mul_zero : ∀ (a : α), a * 0 = 0
                      • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
                      • one : α
                      • one_mul : ∀ (a : α), 1 * a = a
                      • mul_one : ∀ (a : α), a * 1 = a
                      • natCast : α
                      • natCast_zero : 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 = Semiring.npow n x * x
                      • neg : αα
                      • sub : ααα
                      • sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
                      • zsmul : αα
                      • zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
                      • zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = Ring.zsmul (Int.ofNat n) a + 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 bb ca c
                      • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
                      • le_antisymm : ∀ (a b : α), a bb aa = 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 < a0 < b0 < 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 =.

                      Instances

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

                        Instances
                          Equations
                          • =
                          Equations
                          • =
                          Equations
                          • =
                          theorem bit1_mono {α : Type u} [OrderedSemiring α] :
                          @[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 na ^ 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
                          Equations
                          • OrderedRing.toOrderedSemiring = let __src := inst; let __src_1 := Ring.toSemiring; OrderedSemiring.mk
                          Equations
                          • OrderedCommRing.toOrderedCommSemiring = let __src := OrderedRing.toOrderedSemiring; let __src_1 := inst; OrderedCommSemiring.mk
                          @[reducible]

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

                          Equations
                          • StrictOrderedSemiring.toOrderedSemiring' = let __src := inst✝; OrderedSemiring.mk
                          Instances For
                            Equations
                            • StrictOrderedSemiring.toOrderedSemiring = let __src := inst; OrderedSemiring.mk
                            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 < cb < d0 a0 ba * 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) :
                            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) :
                            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) :
                            theorem lt_two_mul_self {α : Type u} [StrictOrderedSemiring α] {a : α} (ha : 0 < a) :
                            a < 2 * a
                            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]

                            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
                            Instances For
                              Equations
                              • StrictOrderedCommSemiring.toOrderedCommSemiring = let __src := inst; let __src_1 := StrictOrderedSemiring.toOrderedSemiring; OrderedCommSemiring.mk
                              Equations
                              • StrictOrderedRing.toStrictOrderedSemiring = let __src := inst; let __src_1 := Ring.toSemiring; StrictOrderedSemiring.mk
                              @[reducible]
                              def StrictOrderedRing.toOrderedRing' {α : Type u} [StrictOrderedRing α] [DecidableRel fun (x x_1 : α) => x x_1] :

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

                              Equations
                              • StrictOrderedRing.toOrderedRing' = let __src := inst✝; let __src_1 := Ring.toSemiring; OrderedRing.mk
                              Instances For
                                Equations
                                • StrictOrderedRing.toOrderedRing = let __spread.0 := inst; OrderedRing.mk
                                @[reducible]

                                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
                                Instances For
                                  Equations
                                  • StrictOrderedCommRing.toStrictOrderedCommSemiring = let __src := inst; let __src_1 := StrictOrderedRing.toStrictOrderedSemiring; StrictOrderedCommSemiring.mk
                                  Equations
                                  • StrictOrderedCommRing.toOrderedCommRing = let __src := inst; let __src_1 := StrictOrderedRing.toOrderedRing; OrderedCommRing.mk
                                  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
                                  Equations
                                  • =
                                  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 < a0 b) (0 < b0 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 pow_two_nonneg {α : Type u} [LinearOrderedSemiring α] [ExistsAddOfLE α] (a : α) :
                                  0 a ^ 2

                                  Alias of sq_nonneg.

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

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  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 < 0b 0) (b < 0a 0)
                                  theorem mul_nonpos_iff_pos_imp_nonpos {α : Type u} [LinearOrderedRing α] {a : α} {b : α} :
                                  a * b 0 (0 < ab 0) (b < 00 a)
                                  theorem mul_nonpos_iff_neg_imp_nonneg {α : Type u} [LinearOrderedRing α] {a : α} {b : α} :
                                  a * b 0 (a < 00 b) (0 < ba 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
                                  Equations
                                  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.