Documentation

Mathlib.Algebra.Order.Monoid.Defs

Ordered monoids #

This file provides the definitions of ordered monoids.

class OrderedCommMonoid (α : Type u_1) extends CommMonoid , PartialOrder :
Type u_1
  • Multiplication is monotone in an OrderedCommMonoid.

    mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b≤ b → c * a ≤ c * b→ c * a ≤ c * b≤ c * b (multiplication is monotone)

Instances
    class OrderedAddCommMonoid (α : Type u_1) extends AddCommMonoid , PartialOrder :
    Type u_1

    An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b≤ b → c + a ≤ c + b→ c + a ≤ c + b≤ c + b (addition is monotone)

    Instances
      def OrderedAddCommMonoid.to_covariantClass_left.proof_1 (M : Type u_1) [inst : OrderedAddCommMonoid M] :
      CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1
      Equations
      def OrderedAddCommMonoid.to_covariantClass_right.proof_1 (M : Type u_1) [inst : OrderedAddCommMonoid M] :
      CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
      Equations
      theorem Add.to_covariantClass_left (M : Type u_1) [inst : Add M] [inst : PartialOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
      CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1
      theorem Mul.to_covariantClass_left (M : Type u_1) [inst : Mul M] [inst : PartialOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
      CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1
      theorem Add.to_covariantClass_right (M : Type u_1) [inst : Add M] [inst : PartialOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
      CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
      theorem Mul.to_covariantClass_right (M : Type u_1) [inst : Mul M] [inst : PartialOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
      CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
      theorem bit0_pos {α : Type u} [inst : OrderedAddCommMonoid α] {a : α} (h : 0 < a) :
      0 < bit0 a

      A linearly ordered additive commutative monoid.

      Instances
        class LinearOrderedCommMonoid (α : Type u_1) extends LinearOrder , CommMonoid :
        Type u_1
        • Multiplication is monotone in an OrderedCommMonoid.

          mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

        A linearly ordered commutative monoid.

        Instances

          A linearly ordered commutative monoid with an additively absorbing ⊤⊤ element. Instances should include number systems with an infinite element adjoined.`

          Instances
            @[simp]
            theorem top_add {α : Type u} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α) :
            @[simp]
            theorem add_top {α : Type u} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α) :