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 = x + AddMonoid.nsmul n 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
    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 = x * Monoid.npow n 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
      instance OrderedAddCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedAddCommMonoid α] :
      CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
      Equations
      instance OrderedCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedCommMonoid α] :
      CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
      Equations
      instance OrderedAddCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedAddCommMonoid M] :
      CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1
      Equations
      • One or more equations did not get rendered due to their size.
      instance OrderedCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedCommMonoid M] :
      CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1
      Equations
      • One or more equations did not get rendered due to their size.

      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 = x + AddMonoid.nsmul n 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
        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 = x * Monoid.npow n 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
          instance OrderedCancelAddCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
          Equations
          instance OrderedCancelCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
          Equations
          instance OrderedCancelAddCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1
          Equations
          instance OrderedCancelCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1
          Equations
          instance OrderedCancelAddCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelAddCommMonoid α] :
          ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1
          Equations
          • One or more equations did not get rendered due to their size.
          instance OrderedCancelCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelCommMonoid α] :
          ContravariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1
          Equations
          • One or more equations did not get rendered due to their size.
          theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) (h : a + b = a + c) :
          b = c
          Equations
          Equations
          • OrderedCancelCommMonoid.toCancelCommMonoid = let src := inst; CancelCommMonoid.mk (_ : ∀ (a b : α), a * b = b * a)
          @[deprecated]
          theorem bit0_pos {α : Type u_1} [OrderedAddCommMonoid α] {a : α} (h : 0 < a) :
          0 < bit0 a
          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 = x + AddMonoid.nsmul n 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 (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 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 = x * Monoid.npow n 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 (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 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 = x + AddMonoid.nsmul n 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 (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 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 = x * Monoid.npow n 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 (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 linearly ordered commutative monoid with an additively absorbing element. Instances should include number systems with an infinite element adjoined.

                  • add : ααα
                  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
                  • zero : α
                  • zero_add : ∀ (a : α), 0 + a = a
                  • add_zero : ∀ (a : α), a + 0 = a
                  • nsmul : αα
                  • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
                  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
                  • add_comm : ∀ (a b : α), a + b = b + a
                  • 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
                  • decidableLE : DecidableRel fun (x x_1 : α) => x x_1
                  • decidableEq : DecidableEq α
                  • decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
                  • min_def : ∀ (a b : α), min a b = if a b then a else b
                  • max_def : ∀ (a b : α), max a b = if a b then b else a
                  • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
                  • top : α
                  • le_top : ∀ (a : α), a
                  • top_add' : ∀ (x : α), + x =

                    In a LinearOrderedAddCommMonoidWithTop, the element is invariant under addition.

                  Instances
                    @[simp]
                    theorem top_add {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
                    @[simp]
                    theorem add_top {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) :
                    @[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