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.

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
    theorem OrderedSemiring.zero_le_one {α : Type u} [self : OrderedSemiring α] :
    0 1

    0 ≤ 1 in any ordered semiring.

    theorem OrderedSemiring.mul_le_mul_of_nonneg_left {α : Type u} [self : OrderedSemiring α] (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.

    theorem OrderedSemiring.mul_le_mul_of_nonneg_right {α : Type u} [self : OrderedSemiring α] (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.

    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.

      • 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 n.succ) a = Ring.zsmul (Int.ofNat n) a + a
      • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
      • neg_add_cancel : ∀ (a : α), -a + a = 0
      • intCast : α
      • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
      • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
      • le : ααProp
      • lt : ααProp
      • le_refl : ∀ (a : α), a a
      • le_trans : ∀ (a b c : α), a 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.

      • zero_le_one : 0 1

        0 ≤ 1 in any ordered ring.

      • mul_nonneg : ∀ (a b : α), 0 a0 b0 a * b

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

      Instances
        theorem OrderedRing.zero_le_one {α : Type u} [self : OrderedRing α] :
        0 1

        0 ≤ 1 in any ordered ring.

        theorem OrderedRing.mul_nonneg {α : Type u} [self : OrderedRing α] (a : α) (b : α) :
        0 a0 b0 a * b

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

        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

            In a strict ordered semiring, 0 ≤ 1.

            theorem StrictOrderedSemiring.mul_lt_mul_of_pos_left {α : Type u} [self : StrictOrderedSemiring α] (a : α) (b : α) (c : α) :
            a < b0 < cc * a < c * b

            Left multiplication by a positive element is strictly monotone.

            theorem StrictOrderedSemiring.mul_lt_mul_of_pos_right {α : Type u} [self : StrictOrderedSemiring α] (a : α) (b : α) (c : α) :
            a < b0 < ca * c < b * c

            Right multiplication by a positive element is strictly monotone.

            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 n.succ) a = Ring.zsmul (Int.ofNat n) a + a
              • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
              • neg_add_cancel : ∀ (a : α), -a + a = 0
              • intCast : α
              • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
              • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
              • le : ααProp
              • lt : ααProp
              • le_refl : ∀ (a : α), a a
              • le_trans : ∀ (a b c : α), a 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
                theorem StrictOrderedRing.zero_le_one {α : Type u} [self : StrictOrderedRing α] :
                0 1

                In a strict ordered ring, 0 ≤ 1.

                theorem StrictOrderedRing.mul_pos {α : Type u} [self : StrictOrderedRing α] (a : α) (b : α) :
                0 < a0 < b0 < 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 = 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 n.succ) a = Ring.zsmul (Int.ofNat n) a + a
                • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
                • neg_add_cancel : ∀ (a : α), -a + a = 0
                • intCast : α
                • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
                • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
                • le : ααProp
                • lt : ααProp
                • le_refl : ∀ (a : α), a a
                • le_trans : ∀ (a b c : α), a 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
                • mul_comm : ∀ (a b : α), a * b = b * a

                  Multiplication is commutative in a commutative multiplicative magma.

                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 (x1 x2 : α) => x1 x2

                    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 (x1 x2 : α) => x1 < x2

                    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 (x1 x2 : α) => x1 x2

                      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 (x1 x2 : α) => x1 < x2

                      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 n.succ) a = Ring.zsmul (Int.ofNat n) a + a
                      • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
                      • neg_add_cancel : ∀ (a : α), -a + a = 0
                      • intCast : α
                      • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
                      • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
                      • le : ααProp
                      • lt : ααProp
                      • le_refl : ∀ (a : α), a a
                      • le_trans : ∀ (a b c : α), a 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 (x1 x2 : α) => x1 x2

                        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 (x1 x2 : α) => x1 < x2

                        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.

                        • 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 n.succ) a = Ring.zsmul (Int.ofNat n) a + a
                        • zsmul_neg' : ∀ (n : ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
                        • neg_add_cancel : ∀ (a : α), -a + a = 0
                        • intCast : α
                        • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
                        • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
                        • le : ααProp
                        • lt : ααProp
                        • le_refl : ∀ (a : α), a a
                        • le_trans : ∀ (a b c : α), a 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
                        • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2
                        • decidableEq : DecidableEq α
                        • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
                        • 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 multiplicative magma.

                        Instances
                          @[instance 100]
                          Equations
                          • =
                          @[instance 200]
                          Equations
                          • =
                          @[instance 200]
                          Equations
                          • =
                          @[instance 100]
                          Equations
                          theorem one_add_le_one_sub_mul_one_add {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : a + b + b * c c) :
                          1 + a (1 - b) * (1 + c)
                          theorem one_add_le_one_add_mul_one_sub {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : a + c + b * c b) :
                          1 + a (1 + b) * (1 - c)
                          theorem one_sub_le_one_sub_mul_one_add {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : b + b * c a + c) :
                          1 - a (1 - b) * (1 + c)
                          theorem one_sub_le_one_add_mul_one_sub {α : Type u} [OrderedRing α] {a : α} {b : α} {c : α} (h : c + b * c a + b) :
                          1 - a (1 + b) * (1 - c)
                          @[instance 100]
                          Equations
                          @[instance 200]
                          Equations
                          • =
                          @[instance 200]
                          Equations
                          • =
                          @[reducible, inline]

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

                          Equations
                          Instances For
                            @[instance 100]
                            Equations
                            @[instance 100]
                            Equations
                            • =
                            @[instance 100]
                            Equations
                            • =
                            @[reducible, inline]

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

                            Equations
                            Instances For
                              @[instance 100]
                              Equations
                              @[instance 100]
                              Equations
                              @[reducible, inline]
                              abbrev StrictOrderedRing.toOrderedRing' {α : Type u} [StrictOrderedRing α] [DecidableRel fun (x1 x2 : α) => x1 x2] :

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

                              Equations
                              Instances For
                                @[instance 100]
                                Equations
                                @[reducible, inline]

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

                                Equations
                                Instances For
                                  @[instance 100]
                                  Equations
                                  @[instance 100]
                                  Equations
                                  @[instance 200]
                                  Equations
                                  • =
                                  @[instance 200]
                                  Equations
                                  • =
                                  @[instance 100]
                                  Equations
                                  • =
                                  @[instance 100]
                                  Equations
                                  • =
                                  @[instance 100]
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  @[instance 100]
                                  Equations
                                  • LinearOrderedRing.toLinearOrderedSemiring = LinearOrderedSemiring.mk LinearOrderedRing.decidableLE LinearOrderedRing.decidableEq LinearOrderedRing.decidableLT
                                  @[instance 100]
                                  Equations
                                  • LinearOrderedRing.toLinearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk LinearOrderedRing.decidableLE LinearOrderedRing.decidableEq LinearOrderedRing.decidableLT
                                  @[instance 100]
                                  Equations
                                  @[instance 100]
                                  Equations
                                  • LinearOrderedCommRing.toLinearOrderedCommSemiring = LinearOrderedCommSemiring.mk LinearOrderedRing.decidableLE LinearOrderedRing.decidableEq LinearOrderedRing.decidableLT