Mathlib.Algebra.Order.Monoid.Defs

IsOrderedAddMonoid structure

(α : Type*) [AddCommMonoid α] [PartialOrder α]

Full source

/-- An ordered (additive) monoid is a monoid with a partial order such that addition is monotone. -/
class IsOrderedAddMonoid (α : Type*) [AddCommMonoid α] [PartialOrder α] where
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c, c + a ≤ c + b
  protected add_le_add_right : ∀ a b : α, a ≤ b → ∀ c, a + c ≤ b + c := fun a b h c ↦ by
    rw [add_comm _ c, add_comm _ c]; exact add_le_add_left a b h c

Ordered additive monoid

Informal description

An ordered additive monoid is an additive commutative monoid $\alpha$ equipped with a partial order such that addition is monotone with respect to the order. That is, for any elements $a, b, c \in \alpha$, if $a \leq b$ then $a + c \leq b + c$ and $c + a \leq c + b$.

IsOrderedMonoid structure

(α : Type*) [CommMonoid α] [PartialOrder α]

Full source

/-- An ordered monoid is a monoid with a partial order such that multiplication is monotone. -/
@[to_additive]
class IsOrderedMonoid (α : Type*) [CommMonoid α] [PartialOrder α] where
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c, c * a ≤ c * b
  protected mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c, a * c ≤ b * c := fun a b h c ↦ by
    rw [mul_comm _ c, mul_comm _ c]; exact mul_le_mul_left a b h c

Ordered Monoid

Informal description

An ordered monoid is a commutative monoid $\alpha$ equipped with a partial order such that the multiplication operation is monotone in both arguments. That is, for any $x, y, z \in \alpha$, if $x \leq y$, then $x \cdot z \leq y \cdot z$ and $z \cdot x \leq z \cdot y$.

IsOrderedMonoid.toMulLeftMono instance

: MulLeftMono α

Full source

@[to_additive]
instance (priority := 900) IsOrderedMonoid.toMulLeftMono : MulLeftMono α where
  elim := fun a _ _ bc ↦ IsOrderedMonoid.mul_le_mul_left _ _ bc a

Left Monotonicity of Multiplication in Ordered Monoids

Informal description

Every ordered monoid $\alpha$ satisfies the property that multiplication is left-monotone, meaning for any $x, y, z \in \alpha$, if $x \leq y$, then $z \cdot x \leq z \cdot y$.

IsOrderedMonoid.toMulRightMono instance

: MulRightMono α

Full source

@[to_additive]
instance (priority := 900) IsOrderedMonoid.toMulRightMono : MulRightMono α where
  elim := fun a _ _ bc ↦ IsOrderedMonoid.mul_le_mul_right _ _ bc a

Right Monotonicity of Multiplication in Ordered Monoids

Informal description

Every ordered monoid $\alpha$ satisfies the property that multiplication is right-monotone, meaning for any $x, y, z \in \alpha$, if $x \leq y$, then $x \cdot z \leq y \cdot z$.

IsOrderedCancelAddMonoid structure

(α : Type*) [AddCommMonoid α] [PartialOrder α] extends
    IsOrderedAddMonoid α

Full source

/-- An ordered cancellative additive monoid is an ordered additive
monoid in which addition is cancellative and monotone. -/
class IsOrderedCancelAddMonoid (α : Type*) [AddCommMonoid α] [PartialOrder α] extends
    IsOrderedAddMonoid α where
  protected le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c
  protected le_of_add_le_add_right : ∀ a b c : α, b + a ≤ c + a → b ≤ c := fun a b c h ↦ by
    rw [add_comm _ a, add_comm _ a] at h; exact le_of_add_le_add_left a b c h

Ordered cancellative additive monoid

Informal description

An ordered cancellative additive monoid is an ordered additive monoid $(α, +, ≤)$ where the addition operation is cancellative (i.e., $a + b = a + c$ implies $b = c$) and monotone (i.e., $a ≤ b$ implies $a + c ≤ b + c$ for all $c$).

IsOrderedCancelMonoid structure

(α : Type*) [CommMonoid α] [PartialOrder α] extends
    IsOrderedMonoid α

Full source

/-- An ordered cancellative monoid is an ordered monoid in which
multiplication is cancellative and monotone. -/
@[to_additive IsOrderedCancelAddMonoid]
class IsOrderedCancelMonoid (α : Type*) [CommMonoid α] [PartialOrder α] extends
    IsOrderedMonoid α where
  protected le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c
  protected le_of_mul_le_mul_right : ∀ a b c : α, b * a ≤ c * a → b ≤ c := fun a b c h ↦ by
    rw [mul_comm _ a, mul_comm _ a] at h; exact le_of_mul_le_mul_left a b c h

Ordered Cancellative Monoid

Informal description

An ordered cancellative monoid is a commutative monoid $\alpha$ equipped with a partial order $\leq$ such that the multiplication operation is cancellative and order-preserving. This means that for any elements $a, b, c \in \alpha$, if $a \cdot c = b \cdot c$ or $c \cdot a = c \cdot b$, then $a = b$, and if $a \leq b$, then $a \cdot c \leq b \cdot c$ and $c \cdot a \leq c \cdot b$.

IsOrderedCancelMonoid.toMulLeftReflectLE instance

: MulLeftReflectLE α

Full source

@[to_additive]
instance (priority := 200) IsOrderedCancelMonoid.toMulLeftReflectLE :
    MulLeftReflectLE α :=
  ⟨IsOrderedCancelMonoid.le_of_mul_le_mul_left⟩

Left multiplication reflects order in ordered cancellative monoids

Informal description

Every ordered cancellative monoid $\alpha$ satisfies the property that multiplication on the left reflects the order relation $\leq$. That is, for any elements $a, b, c \in \alpha$, if $c \cdot a \leq c \cdot b$, then $a \leq b$.

IsOrderedCancelMonoid.toMulLeftReflectLT instance

: MulLeftReflectLT α

Full source

@[to_additive]
instance (priority := 900) IsOrderedCancelMonoid.toMulLeftReflectLT :
    MulLeftReflectLT α where
  elim := contravariant_lt_of_contravariant_le α α _ ContravariantClass.elim

Left Multiplication Reflects Strict Order in Ordered Cancellative Monoids

Informal description

Every ordered cancellative monoid $\alpha$ satisfies the property that multiplication on the left reflects the strict order relation $<$. That is, for any elements $a, b, c \in \alpha$, if $c \cdot a < c \cdot b$, then $a < b$.

IsOrderedCancelMonoid.toMulRightReflectLT theorem

: MulRightReflectLT α

Full source

@[to_additive]
theorem IsOrderedCancelMonoid.toMulRightReflectLT :
    MulRightReflectLT α :=
  inferInstance

Right Multiplication Reflects Strict Order in Ordered Cancellative Monoids

Informal description

Every ordered cancellative monoid $\alpha$ satisfies the property that multiplication on the right reflects the strict order relation $<$. That is, for any elements $a, b, c \in \alpha$, if $a \cdot c < b \cdot c$, then $a < b$.

IsOrderedCancelMonoid.toIsCancelMul instance

: IsCancelMul α

Full source

@[to_additive IsOrderedCancelAddMonoid.toIsCancelAdd]
instance (priority := 100) IsOrderedCancelMonoid.toIsCancelMul : IsCancelMul α where
  mul_left_cancel _ _ _ h :=
    (le_of_mul_le_mul_left' h.le).antisymm <| le_of_mul_le_mul_left' h.ge
  mul_right_cancel _ _ _ h :=
    (le_of_mul_le_mul_right' h.le).antisymm <| le_of_mul_le_mul_right' h.ge

Ordered Cancellative Monoids are Cancellative Monoids

Informal description

Every ordered cancellative monoid $\alpha$ is a cancellative monoid.

OrderedAddCommMonoid structure

(α : Type*) extends AddCommMonoid α, PartialOrder α

Full source

/-- An ordered (additive) commutative monoid is a commutative monoid with a partial order such that
addition is monotone. -/
@[deprecated "Use `[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedAddCommMonoid (α : Type*) extends AddCommMonoid α, PartialOrder α where
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c, c + a ≤ c + b

Ordered additive commutative monoid

Informal description

An ordered additive commutative monoid is a commutative monoid $\alpha$ equipped with a partial order $\leq$ such that addition is monotone, i.e., for any $a, b, c \in \alpha$, if $a \leq b$ then $a + c \leq b + c$.

OrderedCommMonoid structure

(α : Type*) extends CommMonoid α, PartialOrder α

Full source

/-- An ordered commutative monoid is a commutative monoid with a partial order such that
multiplication is monotone. -/
@[to_additive,
  deprecated "Use `[CommMonoid α] [PartialOrder α] [IsOrderedMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedCommMonoid (α : Type*) extends CommMonoid α, PartialOrder α where
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c, c * a ≤ c * b

Ordered commutative monoid

Informal description

An ordered commutative monoid is a commutative monoid $\alpha$ equipped with a partial order $\leq$ such that the multiplication operation is monotone with respect to $\leq$, i.e., for all $a, b, c \in \alpha$, if $a \leq b$ then $a \cdot c \leq b \cdot c$ and $c \cdot a \leq c \cdot b$.

OrderedCancelAddCommMonoid structure

(α : Type*) extends OrderedAddCommMonoid α

Full source

/-- An ordered cancellative additive commutative monoid is a partially ordered commutative additive
monoid in which addition is cancellative and monotone. -/
@[deprecated "Use `[AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedCancelAddCommMonoid (α : Type*) extends OrderedAddCommMonoid α where
  protected le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c

Ordered cancellative additive commutative monoid

Informal description

An ordered cancellative additive commutative monoid is a partially ordered commutative additive monoid in which addition is cancellative (i.e., $a + b = a + c$ implies $b = c$) and monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ for all $c$).

OrderedCancelCommMonoid structure

(α : Type*) extends OrderedCommMonoid α

Full source

/-- An ordered cancellative commutative monoid is a partially ordered commutative monoid in which
multiplication is cancellative and monotone. -/
@[to_additive OrderedCancelAddCommMonoid,
  deprecated "Use `[CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedCancelCommMonoid (α : Type*) extends OrderedCommMonoid α where
  protected le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c

Ordered cancellative commutative monoid

Informal description

An ordered cancellative commutative monoid is a commutative monoid $\alpha$ equipped with a partial order such that multiplication is cancellative (i.e., $a \cdot b = a \cdot c$ implies $b = c$) and monotone (i.e., $a \leq b$ implies $a \cdot c \leq b \cdot c$ for all $c$).

LinearOrderedAddCommMonoid structure

(α : Type*) extends OrderedAddCommMonoid α, LinearOrder α

Full source

/-- A linearly ordered additive commutative monoid. -/
@[deprecated "Use `[AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedAddCommMonoid (α : Type*) extends OrderedAddCommMonoid α, LinearOrder α

Linearly Ordered Additive Commutative Monoid

Informal description

A linearly ordered additive commutative monoid is a structure that combines the properties of an ordered additive commutative monoid and a linear order on the underlying type $\alpha$. This means that $\alpha$ is equipped with a commutative addition operation, a neutral element for addition, and a linear order relation that is compatible with the addition operation.

LinearOrderedCommMonoid structure

(α : Type*) extends OrderedCommMonoid α, LinearOrder α

Full source

/-- A linearly ordered commutative monoid. -/
@[to_additive,
  deprecated "Use `[CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCommMonoid (α : Type*) extends OrderedCommMonoid α, LinearOrder α

Linearly Ordered Commutative Monoid

Informal description

A linearly ordered commutative monoid is a structure consisting of a commutative monoid $\alpha$ equipped with a linear order such that the multiplication operation is monotone (i.e., for all $a, b, c \in \alpha$, if $a \leq b$ then $a \cdot c \leq b \cdot c$).

LinearOrderedCancelAddCommMonoid structure

(α : Type*) extends OrderedCancelAddCommMonoid α,
    LinearOrderedAddCommMonoid α

Full source

/-- A linearly ordered cancellative additive commutative monoid is an additive commutative monoid
with a decidable linear order in which addition is cancellative and monotone. -/
@[deprecated "Use `[AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCancelAddCommMonoid (α : Type*) extends OrderedCancelAddCommMonoid α,
    LinearOrderedAddCommMonoid α

Linearly Ordered Cancellative Additive Commutative Monoid

Informal description

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone. This means that for any elements $a, b, c$ in the monoid, if $a + b = a + c$, then $b = c$ (cancellativity), and if $a \leq b$, then $a + c \leq b + c$ (monotonicity).

LinearOrderedCancelCommMonoid structure

(α : Type*) extends OrderedCancelCommMonoid α,
    LinearOrderedCommMonoid α

Full source

/-- A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order
in which multiplication is cancellative and monotone. -/
@[to_additive LinearOrderedCancelAddCommMonoid,
  deprecated "Use `[CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCancelCommMonoid (α : Type*) extends OrderedCancelCommMonoid α,
    LinearOrderedCommMonoid α

Linearly ordered cancellative commutative monoid

Informal description

A linearly ordered cancellative commutative monoid is a commutative monoid $\alpha$ equipped with a linear order, where the multiplication operation is cancellative (i.e., $a \cdot c = b \cdot c$ implies $a = b$) and monotone (i.e., $a \leq b$ implies $a \cdot c \leq b \cdot c$ for all $c$).

one_le_mul_self_iff theorem

: 1 ≤ a * a ↔ 1 ≤ a

Full source

@[to_additive (attr := simp)]
theorem one_le_mul_self_iff : 1 ≤ a * a ↔ 1 ≤ a :=
  ⟨(fun h ↦ by push_neg at h ⊢; exact mul_lt_one' h h).mtr, fun h ↦ one_le_mul h h⟩

Square Inequality in Ordered Monoid: $1 \leq a^2 \leftrightarrow 1 \leq a$

Informal description

For any element $a$ in an ordered monoid, the inequality $1 \leq a^2$ holds if and only if $1 \leq a$.

one_lt_mul_self_iff theorem

: 1 < a * a ↔ 1 < a

Full source

@[to_additive (attr := simp)]
theorem one_lt_mul_self_iff : 1 < a * a ↔ 1 < a :=
  ⟨(fun h ↦ by push_neg at h ⊢; exact mul_le_one' h h).mtr, fun h ↦ one_lt_mul'' h h⟩

Square Strict Inequality in Ordered Monoid: $1 < a^2 \leftrightarrow 1 < a$

Informal description

For any element $a$ in an ordered monoid, the inequality $1 < a^2$ holds if and only if $1 < a$.

mul_self_le_one_iff theorem

: a * a ≤ 1 ↔ a ≤ 1

Full source

@[to_additive (attr := simp)]
theorem mul_self_le_one_iff : a * a ≤ 1 ↔ a ≤ 1 := by simp [← not_iff_not]

Square Inequality in Ordered Monoid: $a^2 \leq 1 \leftrightarrow a \leq 1$

Informal description

For any element $a$ in an ordered monoid, the square of $a$ is less than or equal to the multiplicative identity if and only if $a$ itself is less than or equal to the multiplicative identity, i.e., $a^2 \leq 1 \leftrightarrow a \leq 1$.

mul_self_lt_one_iff theorem

: a * a < 1 ↔ a < 1

Full source

@[to_additive (attr := simp)]
theorem mul_self_lt_one_iff : a * a < 1 ↔ a < 1 := by simp [← not_iff_not]

Square Less Than One iff Element Less Than One in Ordered Monoid

Informal description

For any element $a$ in an ordered monoid $\alpha$, the square of $a$ is less than $1$ if and only if $a$ is less than $1$, i.e., $a^2 < 1 \leftrightarrow a < 1$.