Documentation

Mathlib.Algebra.Order.Monoid.Defs

Ordered monoids #

This file provides the definitions of ordered monoids.

class OrderedAddCommMonoid (α : Type u_3) extends AddCommMonoid , PartialOrder :
Type u_3

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that addition 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
  • 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
Instances
    theorem OrderedAddCommMonoid.add_le_add_left {α : Type u_3} [self : OrderedAddCommMonoid α] (a : α) (b : α) :
    a b∀ (c : α), c + a c + b
    class OrderedCommMonoid (α : Type u_3) extends CommMonoid , PartialOrder :
    Type u_3

    An ordered commutative monoid is a commutative monoid with a partial order such that multiplication is monotone.

    • mul : ααα
    • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
    • one : α
    • one_mul : ∀ (a : α), 1 * a = a
    • mul_one : ∀ (a : α), a * 1 = a
    • npow : αα
    • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
    • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
    • mul_comm : ∀ (a b : α), a * b = b * a
    • 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
    • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
    Instances
      theorem OrderedCommMonoid.mul_le_mul_left {α : Type u_3} [self : OrderedCommMonoid α] (a : α) (b : α) :
      a b∀ (c : α), c * a c * b
      instance OrderedAddCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedAddCommMonoid α] :
      CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2
      Equations
      • =
      instance OrderedCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedCommMonoid α] :
      CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2
      Equations
      • =
      theorem OrderedAddCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedAddCommMonoid M] :
      CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2
      theorem OrderedCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedCommMonoid M] :
      CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2

      An ordered cancellative additive commutative monoid is a partially ordered commutative additive monoid in which addition is cancellative and 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
      • 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
      Instances
        theorem OrderedCancelAddCommMonoid.le_of_add_le_add_left {α : Type u_3} [self : OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) :
        a + b a + cb c
        class OrderedCancelCommMonoid (α : Type u_3) extends OrderedCommMonoid :
        Type u_3

        An ordered cancellative commutative monoid is a partially ordered commutative monoid in which multiplication is cancellative and monotone.

        • mul : ααα
        • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
        • one : α
        • one_mul : ∀ (a : α), 1 * a = a
        • mul_one : ∀ (a : α), a * 1 = a
        • npow : αα
        • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
        • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
        • mul_comm : ∀ (a b : α), a * b = b * a
        • 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
        • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
        • le_of_mul_le_mul_left : ∀ (a b c : α), a * b a * cb c
        Instances
          theorem OrderedCancelCommMonoid.le_of_mul_le_mul_left {α : Type u_3} [self : OrderedCancelCommMonoid α] (a : α) (b : α) (c : α) :
          a * b a * cb c
          @[instance 200]
          instance OrderedCancelAddCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2
          Equations
          • =
          @[instance 200]
          instance OrderedCancelCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2
          Equations
          • =
          instance OrderedCancelAddCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2
          Equations
          • =
          instance OrderedCancelCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2
          Equations
          • =
          theorem OrderedCancelAddCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2
          theorem OrderedCancelCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2
          @[instance 100]
          Equations
          theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) (h : a + b = a + c) :
          b = c
          @[instance 100]
          Equations
          class LinearOrderedAddCommMonoid (α : Type u_3) extends OrderedAddCommMonoid , Min , Max , Ord :
          Type u_3

          A linearly ordered additive commutative monoid.

          • 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
          • 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
          • 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 LinearOrderedCommMonoid (α : Type u_3) extends OrderedCommMonoid , Min , Max , Ord :
            Type u_3

            A linearly ordered commutative monoid.

            • mul : ααα
            • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
            • one : α
            • one_mul : ∀ (a : α), 1 * a = a
            • mul_one : ∀ (a : α), a * 1 = a
            • npow : αα
            • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
            • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
            • mul_comm : ∀ (a b : α), a * b = b * a
            • 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
            • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * 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 linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and 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
              • 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
              • 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 linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

                • mul : ααα
                • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
                • one : α
                • one_mul : ∀ (a : α), 1 * a = a
                • mul_one : ∀ (a : α), a * 1 = a
                • npow : αα
                • npow_zero : ∀ (x : α), Monoid.npow 0 x = 1
                • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n x * x
                • mul_comm : ∀ (a b : α), a * b = b * a
                • 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
                • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
                • le_of_mul_le_mul_left : ∀ (a b c : α), a * b a * cb 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
                  @[simp]
                  theorem nonneg_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
                  0 a + a 0 a
                  @[simp]
                  theorem one_le_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
                  1 a * a 1 a
                  @[simp]
                  theorem pos_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
                  0 < a + a 0 < a
                  @[simp]
                  theorem one_lt_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
                  1 < a * a 1 < a
                  @[simp]
                  theorem add_self_nonpos_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
                  a + a 0 a 0
                  @[simp]
                  theorem mul_self_le_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
                  a * a 1 a 1
                  @[simp]
                  theorem add_self_neg_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} :
                  a + a < 0 a < 0
                  @[simp]
                  theorem mul_self_lt_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} :
                  a * a < 1 a < 1