Ordered monoids

This file provides the definitions of ordered monoids.

class 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

class 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

instance OrderedCommMonoid.toMulLeftMono {α : Type u_1} [OrderedCommMonoid α] : MulLeftMono α

Equations

• ⋯ = ⋯

instance OrderedAddCommMonoid.toAddLeftMono {α : Type u_1} [OrderedAddCommMonoid α] : AddLeftMono α

Equations

• ⋯ = ⋯

theorem OrderedCommMonoid.toMulRightMono (M : Type u_2) [OrderedCommMonoid M] : MulRightMono M

theorem OrderedAddCommMonoid.toAddRightMono (M : Type u_2) [OrderedAddCommMonoid M] : AddRightMono M

class 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

class 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

@[instance 200]

instance OrderedCancelCommMonoid.toMulLeftReflectLE {α : Type u_1} [OrderedCancelCommMonoid α] : MulLeftReflectLE α

Equations

• ⋯ = ⋯

@[instance 200]

instance OrderedCancelAddCommMonoid.toAddLeftReflectLE {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddLeftReflectLE α

Equations

• ⋯ = ⋯

instance OrderedCancelCommMonoid.toMulLeftReflectLT {α : Type u_1} [OrderedCancelCommMonoid α] : MulLeftReflectLT α

Equations

• ⋯ = ⋯

instance OrderedCancelAddCommMonoid.toAddLeftReflectLT {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddLeftReflectLT α

Equations

• ⋯ = ⋯

theorem OrderedCancelCommMonoid.toMulRightReflectLT {α : Type u_1} [OrderedCancelCommMonoid α] : MulRightReflectLT α

theorem OrderedCancelAddCommMonoid.toAddRightReflectLT {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddRightReflectLT α

@[instance 100]

instance OrderedCancelCommMonoid.toCancelCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] : CancelCommMonoid α

Equations

• OrderedCancelCommMonoid.toCancelCommMonoid = CancelCommMonoid.mk ⋯

@[instance 100]

instance OrderedCancelAddCommMonoid.toCancelAddCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddCancelCommMonoid α

Equations

• OrderedCancelAddCommMonoid.toCancelAddCommMonoid = AddCancelCommMonoid.mk ⋯

class 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
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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

class 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
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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

class 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
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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

class 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
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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} [LinearOrderedCommMonoid α] {a : α} : 1 ≤ a * a ↔ 1 ≤ a

@[simp]

theorem nonneg_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 pos_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : 0 < a + a ↔ 0 < a

@[simp]

theorem mul_self_le_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : a * a ≤ 1 ↔ a ≤ 1

@[simp]

theorem add_self_nonpos_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

@[simp]

theorem add_self_neg_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : a + a < 0 ↔ a < 0