Ordered monoids

This file provides the definitions of ordered monoids.

class IsOrderedAddMonoid (α : Type u_2) [AddCommMonoid α] [Preorder α] : Prop

An ordered (additive) monoid is a monoid with a preorder such that addition is monotone.

• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

class IsOrderedMonoid (α : Type u_2) [CommMonoid α] [Preorder α] : Prop

An ordered monoid is a monoid with a preorder such that multiplication is monotone.

• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), a * c ≤ b * c
• mul_le_mul_right (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b

@[instance 900]

instance IsOrderedMonoid.toMulLeftMono {α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : MulLeftMono α

@[instance 900]

instance IsOrderedAddMonoid.toAddLeftMono {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : AddLeftMono α

@[instance 900]

instance IsOrderedMonoid.toMulRightMono {α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : MulRightMono α

@[instance 900]

instance IsOrderedAddMonoid.toAddRightMono {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : AddRightMono α

class IsOrderedCancelAddMonoid (α : Type u_2) [AddCommMonoid α] [Preorder α] extends IsOrderedAddMonoid α : Prop

An ordered cancellative additive monoid is an ordered additive monoid in which addition is cancellative and monotone.

• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• le_of_add_le_add_right (a b c : α) : b + a ≤ c + a → b ≤ c

class IsOrderedCancelMonoid (α : Type u_2) [CommMonoid α] [Preorder α] extends IsOrderedMonoid α : Prop

An ordered cancellative monoid is an ordered monoid in which multiplication is cancellative and monotone.

• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), a * c ≤ b * c
• mul_le_mul_right (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b
• le_of_mul_le_mul_left (a b c : α) : a * b ≤ a * c → b ≤ c
• le_of_mul_le_mul_right (a b c : α) : b * a ≤ c * a → b ≤ c

instance instOrderedAddOfIsOrderedCancelAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : Lean.Grind.OrderedAdd α

@[instance 200]

instance IsOrderedCancelMonoid.toMulLeftReflectLE {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedCancelMonoid α] : MulLeftReflectLE α

@[instance 200]

instance IsOrderedCancelAddMonoid.toAddLeftReflectLE {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] : AddLeftReflectLE α

@[instance 900]

instance IsOrderedCancelMonoid.toMulLeftReflectLT {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : MulLeftReflectLT α

@[instance 900]

instance IsOrderedCancelAddMonoid.toAddLeftReflectLT {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : AddLeftReflectLT α

theorem IsOrderedCancelMonoid.toMulRightReflectLT {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : MulRightReflectLT α

theorem IsOrderedCancelAddMonoid.toAddRightReflectLT {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : AddRightReflectLT α

@[instance 100]

instance IsOrderedCancelMonoid.toIsCancelMul {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : IsCancelMul α

@[instance 100]

instance IsOrderedCancelAddMonoid.toIsCancelAdd {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] : IsCancelAdd α

theorem IsOrderedCancelMonoid.of_mul_lt_mul_left {α : Type u_2} [CommMonoid α] [LinearOrder α] (hmul : ∀ (a b c : α), b < c → a * b < a * c) : IsOrderedCancelMonoid α

theorem IsOrderedCancelAddMonoid.of_add_lt_add_left {α : Type u_2} [AddCommMonoid α] [LinearOrder α] (hadd : ∀ (a b c : α), b < c → a + b < a + c) : IsOrderedCancelAddMonoid α

@[simp]

theorem one_le_mul_self_iff {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : 1 ≤ a * a ↔ 1 ≤ a

@[simp]

theorem nonneg_add_self_iff {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : 0 ≤ a + a ↔ 0 ≤ a

@[simp]

theorem one_lt_mul_self_iff {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : 1 < a * a ↔ 1 < a

@[simp]

theorem pos_add_self_iff {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : 0 < a + a ↔ 0 < a

@[simp]

theorem mul_self_le_one_iff {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a * a ≤ 1 ↔ a ≤ 1

@[simp]

theorem add_self_nonpos_iff {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a + a ≤ 0 ↔ a ≤ 0

@[simp]

theorem mul_self_lt_one_iff {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a * a < 1 ↔ a < 1

@[simp]

theorem add_self_neg_iff {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a + a < 0 ↔ a < 0