Ordered monoids

This file provides the definitions of ordered monoids.

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

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

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

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

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

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

@[instance 900]

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

@[instance 900]

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

@[instance 900]

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

@[instance 900]

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

class IsOrderedCancelAddMonoid (α : Type u_2) [AddCommMonoid α] [PartialOrder α] 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 : α), c + a ≤ c + b
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• 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 α] [PartialOrder α] 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 : α), c * a ≤ c * b
• mul_le_mul_right (a b : α) : a ≤ b → ∀ (c : α), a * c ≤ b * c
• 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 200]

instance IsOrderedCancelMonoid.toMulLeftReflectLE {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : MulLeftReflectLE α

@[instance 200]

instance IsOrderedCancelAddMonoid.toAddLeftReflectLE {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [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 α

@[deprecated "Use `[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure OrderedAddCommMonoid (α : Type u_2) extends AddCommMonoid α, PartialOrder α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

@[deprecated "Use `[CommMonoid α] [PartialOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure OrderedCommMonoid (α : Type u_2) extends CommMonoid α, PartialOrder α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b

@[deprecated "Use `[AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]` instead." (since := "2025-04-10")]

structure OrderedCancelAddCommMonoid (α : Type u_2) extends OrderedAddCommMonoid α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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 + c → b ≤ c

@[deprecated "Use `[CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α]` instead." (since := "2025-04-10")]

structure OrderedCancelCommMonoid (α : Type u_2) extends OrderedCommMonoid α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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 * c → b ≤ c

@[deprecated "Use `[AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedAddCommMonoid (α : Type u_2) extends OrderedAddCommMonoid α, LinearOrder α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedCommMonoid (α : Type u_2) extends OrderedCommMonoid α, LinearOrder α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedCancelAddCommMonoid (α : Type u_2) extends OrderedCancelAddCommMonoid α, LinearOrderedAddCommMonoid α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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 + c → b ≤ c
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedCancelCommMonoid (α : Type u_2) extends OrderedCancelCommMonoid α, LinearOrderedCommMonoid α : Type u_2

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = 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 * c → b ≤ c
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[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