mathlib documentation

algebra.order.monoid

Ordered monoids #

This file develops the basics of ordered monoids.

Implementation details #

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

@[instance]
@[instance]
@[class]
structure ordered_comm_monoid (α : Type u_1) :
Type u_1
  • 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 : α), ordered_comm_monoid.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), ordered_comm_monoid.npow n.succ x = x * ordered_comm_monoid.npow n x) . "try_refl_tac"
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • 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 (multiplication is monotone)

Instances
@[instance]
@[class]
structure ordered_add_comm_monoid (α : Type u_1) :
Type u_1
  • 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 : α), ordered_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), ordered_add_comm_monoid.nsmul n.succ x = x + ordered_add_comm_monoid.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b

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

Instances
@[class]
structure has_exists_mul_of_le (α : Type u) [ordered_comm_monoid α] :
Prop
  • exists_mul_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a * c)

An ordered_comm_monoid with one-sided 'division' in the sense that if a ≤ b, there is some c for which a * c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_monoid.

Instances
@[class]
structure has_exists_add_of_le (α : Type u) [ordered_add_comm_monoid α] :
Prop
  • exists_add_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a + c)

An ordered_add_comm_monoid with one-sided 'subtraction' in the sense that if a ≤ b, then there is some c for which a + c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_add_monoid.

Instances
@[class]
structure linear_ordered_add_comm_monoid (α : Type u_1) :
Type u_1

A linearly ordered additive commutative monoid.

Instances
@[class]
structure linear_ordered_comm_monoid (α : Type u_1) :
Type u_1

A linearly ordered commutative monoid.

Instances
@[class]
structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :
Type u_1

A linearly ordered commutative monoid with a zero element.

Instances
@[class]
structure linear_ordered_add_comm_monoid_with_top (α : Type u_1) :
Type u_1

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} [linear_ordered_add_comm_monoid_with_top α] (a : α) :
@[simp]
theorem add_top {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :
def function.injective.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback an ordered_comm_monoid under an injective map. See note [reducible non-instances].

Equations
def function.injective.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

Pullback an ordered_add_comm_monoid under an injective map.

Equations
theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} (h : 0 < a) :
0 < bit0 a
@[protected, instance]
def add_units.preorder {α : Type u} [add_monoid α] [preorder α] :
Equations
@[protected, instance]
def units.preorder {α : Type u} [monoid α] [preorder α] :
Equations
@[simp, norm_cast]
theorem add_units.coe_le_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
a b a b
@[simp, norm_cast]
theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a b a b
@[simp, norm_cast]
theorem add_units.coe_lt_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
a < b a < b
@[simp, norm_cast]
theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a < b a < b
@[protected, instance]
def units.partial_order {α : Type u} [monoid α] [partial_order α] :
Equations
@[protected, instance]
def units.linear_order {α : Type u} [monoid α] [linear_order α] :
Equations
@[simp, norm_cast]
theorem add_units.max_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
(max a b) = max a b
@[simp, norm_cast]
theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(max a b) = max a b
@[simp, norm_cast]
theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(min a b) = min a b
@[simp, norm_cast]
theorem add_units.min_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
(min a b) = min a b
@[protected, instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_zero.order_bot {α : Type u} [partial_order α] :
Equations
theorem with_zero.zero_le {α : Type u} [partial_order α] (a : with_zero α) :
0 a
theorem with_zero.zero_lt_coe {α : Type u} [preorder α] (a : α) :
0 < a
@[simp, norm_cast]
theorem with_zero.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :
a < b a < b
@[simp, norm_cast]
theorem with_zero.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
a b a b
@[protected, instance]
def with_zero.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
Equations
theorem with_zero.mul_le_mul_left {α : Type u} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] (a b : with_zero α) :
a b∀ (c : with_zero α), c * a c * b
theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} [has_mul α] [partial_order α] [contravariant_class α α has_mul.mul has_lt.lt] (a b c : with_zero α) :
a * b < a * cb < c
@[protected, instance]
def with_top.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
def with_top.has_zero {α : Type u} [has_zero α] :
Equations
@[simp, norm_cast]
theorem with_top.coe_one {α : Type u} [has_one α] :
1 = 1
@[simp, norm_cast]
theorem with_top.coe_zero {α : Type u} [has_zero α] :
0 = 0
@[simp, norm_cast]
theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
a = 0 a = 0
@[simp, norm_cast]
theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :
a = 1 a = 1
@[simp, norm_cast]
theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :
0 = a a = 0
@[simp, norm_cast]
theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :
1 = a a = 1
@[simp]
theorem with_top.top_ne_one {α : Type u} [has_one α] :
@[simp]
theorem with_top.top_ne_zero {α : Type u} [has_zero α] :
@[simp]
theorem with_top.zero_ne_top {α : Type u} [has_zero α] :
@[simp]
theorem with_top.one_ne_top {α : Type u} [has_one α] :
@[protected, instance]
def with_top.has_add {α : Type u} [has_add α] :
Equations
@[norm_cast]
theorem with_top.coe_add {α : Type u} [has_add α] {a b : α} :
(a + b) = a + b
@[norm_cast]
theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :
@[norm_cast]
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
@[simp]
theorem with_top.add_top {α : Type u} [has_add α] {a : with_top α} :
@[simp]
theorem with_top.top_add {α : Type u} [has_add α] {a : with_top α} :
theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :
a + b = a = b =
theorem with_top.add_lt_top {α : Type u} [has_add α] [partial_order α] {a b : with_top α} :
a + b < a < b <
theorem with_top.add_eq_coe {α : Type u} [has_add α] {a b : with_top α} {c : α} :
a + b = c ∃ (a' b' : α), a' = a b' = b a' + b' = c
@[simp]
theorem with_top.add_coe_eq_top_iff {α : Type u} [has_add α] {x : with_top α} {y : α} :
x + y = x =
@[simp]
theorem with_top.coe_add_eq_top_iff {α : Type u} [has_add α] {x : α} {y : with_top α} :
x + y = y =
@[protected, instance]
Equations
def with_top.coe_add_hom {α : Type u} [add_monoid α] :

Coercion from α to with_top α as an add_monoid_hom.

Equations
@[simp]
@[simp]
theorem with_top.zero_lt_top {α : Type u} [ordered_add_comm_monoid α] :
0 <
@[simp, norm_cast]
theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :
0 < a 0 < a
@[protected, instance]
def with_bot.has_zero {α : Type u} [has_zero α] :
Equations
@[protected, instance]
def with_bot.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def with_bot.add_monoid {α : Type u} [add_monoid α] :
Equations
theorem with_bot.coe_zero {α : Type u} [has_zero α] :
0 = 0
theorem with_bot.coe_one {α : Type u} [has_one α] :
1 = 1
theorem with_bot.coe_eq_zero {α : Type u_1} [add_monoid α] {a : α} :
a = 0 a = 0
theorem with_bot.coe_add {α : Type u} [add_semigroup α] (a b : α) :
(a + b) = a + b
theorem with_bot.coe_bit0 {α : Type u} [add_semigroup α] {a : α} :
theorem with_bot.coe_bit1 {α : Type u} [add_semigroup α] [has_one α] {a : α} :
@[simp]
theorem with_bot.bot_add {α : Type u} [add_semigroup α] (a : with_bot α) :
@[simp]
theorem with_bot.add_bot {α : Type u} [add_semigroup α] (a : with_bot α) :
@[simp]
theorem with_bot.add_eq_bot {α : Type u} [add_semigroup α] {m n : with_bot α} :
m + n = m = n =
@[class]
structure canonically_ordered_add_monoid (α : Type u_1) :
Type u_1

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the subtractibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial ordered_add_comm_groups.

Instances
@[instance]
@[class]
structure canonically_ordered_monoid (α : Type u_1) :
Type u_1
  • 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 : α), canonically_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), canonically_ordered_monoid.npow n.succ x = x * canonically_ordered_monoid.npow n x) . "try_refl_tac"
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
  • bot : α
  • bot_le : ∀ (x : α), x
  • le_iff_exists_mul : ∀ (a b : α), a b ∃ (c : α), b = a * c

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a * c. Examples seem rare; it seems more likely that the order_dual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

Instances
theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b ∃ (c : α), b = a + c
theorem le_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b ∃ (c : α), b = a * c
theorem self_le_mul_right {α : Type u} [canonically_ordered_monoid α] (a b : α) :
a a * b
theorem self_le_add_right {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :
a a + b
theorem self_le_add_left {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :
a b + a
theorem self_le_mul_left {α : Type u} [canonically_ordered_monoid α] (a b : α) :
a b * a
@[simp]
theorem one_le {α : Type u} [canonically_ordered_monoid α] (a : α) :
1 a
@[simp]
theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :
0 a
@[simp]
theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :
= 1
@[simp]
theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :
= 0
@[simp]
theorem mul_eq_one_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a * b = 1 a = 1 b = 1
@[simp]
theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a + b = 0 a = 0 b = 0
@[simp]
theorem le_one_iff_eq_one {α : Type u} [canonically_ordered_monoid α] {a : α} :
a 1 a = 1
@[simp]
theorem nonpos_iff_eq_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
a 0 a = 0
theorem one_lt_iff_ne_one {α : Type u} [canonically_ordered_monoid α] {a : α} :
1 < a a 1
theorem pos_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
0 < a a 0
theorem exists_pos_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :
∃ (c : α) (H : c > 1), a * c = b
theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :
∃ (c : α) (H : c > 0), a + c = b
theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a c) :
a b + c
theorem le_mul_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a c) :
a b * c
theorem le_mul_self {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b * a
theorem le_add_self {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b + a
theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a b) :
a b + c
theorem le_mul_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a b) :
a b * c
theorem le_self_mul {α : Type u} [canonically_ordered_monoid α] {a c : α} :
a a * c
theorem le_self_add {α : Type u} [canonically_ordered_add_monoid α] {a c : α} :
a a + c
theorem lt_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} [covariant_class α α has_mul.mul has_lt.lt] :
a < b ∃ (c : α) (H : c > 1), b = a * c
theorem lt_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} [covariant_class α α has_add.add has_lt.lt] :
a < b ∃ (c : α) (H : c > 0), b = a + c
theorem pos_of_gt {M : Type u_1} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) :
0 < m
@[class]
structure canonically_linear_ordered_add_monoid (α : Type u_1) :
Type u_1

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

Instances
@[class]
structure canonically_linear_ordered_monoid (α : Type u_1) :
Type u_1

A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.

theorem min_add_distrib {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :
min a (b + c) = min a (min a b + min a c)
theorem min_mul_distrib {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :
min a (b * c) = min a ((min a b) * min a c)
theorem min_mul_distrib' {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :
min (a * b) c = min ((min a c) * min b c) c
theorem min_add_distrib' {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :
min (a + b) c = min (min a c + min b c) c
@[simp]
theorem one_min {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
min 1 a = 1
@[simp]
theorem zero_min {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
min 0 a = 0
@[simp]
theorem min_zero {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
min a 0 = 0
@[simp]
theorem min_one {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
min a 1 = 1
@[class]
structure ordered_cancel_add_comm_monoid (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • add_left_cancel : ∀ (a b c : α), a + b = a + cb = c
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : α → α
  • nsmul_zero' : (∀ (x : α), ordered_cancel_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), ordered_cancel_add_comm_monoid.nsmul n.succ x = x + ordered_cancel_add_comm_monoid.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = 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 + cb c

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

Instances
@[class]
structure ordered_cancel_comm_monoid (α : Type u) :
Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • mul_left_cancel : ∀ (a b c : α), a * b = a * cb = c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : α → α
  • npow_zero' : (∀ (x : α), ordered_cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), ordered_cancel_comm_monoid.npow n.succ x = x * ordered_cancel_comm_monoid.npow n x) . "try_refl_tac"
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = 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 * cb c

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and monotone.

Instances
theorem ordered_cancel_add_comm_monoid.lt_of_add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a b c : α) :
a + b < a + cb < c
theorem ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left {α : Type u} [ordered_cancel_comm_monoid α] (a b c : α) :
a * b < a * cb < c

Some lemmas about types that have an ordering and a binary operation, with no rules relating them.

theorem fn_min_mul_fn_max {α : Type u} {β : Type u_1} [linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :
(f (min n m)) * f (max n m) = (f n) * f m
theorem fn_min_add_fn_max {α : Type u} {β : Type u_1} [linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :
f (min n m) + f (max n m) = f n + f m
theorem min_add_max {α : Type u} [linear_order α] [add_comm_semigroup α] (n m : α) :
min n m + max n m = n + m
theorem min_mul_max {α : Type u} [linear_order α] [comm_semigroup α] (n m : α) :
(min n m) * max n m = n * m
@[class]
structure linear_ordered_cancel_add_comm_monoid (α : Type u) :
Type u

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

Instances
@[class]
structure linear_ordered_cancel_comm_monoid (α : Type u) :
Type u

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

Instances
theorem min_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
min (a * b) (a * c) = a * min b c
theorem min_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
min (a + b) (a + c) = a + min b c
theorem max_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
max (a + b) (a + c) = a + max b c
theorem max_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
max (a * b) (a * c) = a * max b c
theorem min_add_add_right {α : Type u} [linear_order α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b c : α) :
min (a + c) (b + c) = min a b + c
theorem min_mul_mul_right {α : Type u} [linear_order α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b c : α) :
min (a * c) (b * c) = (min a b) * c
theorem max_mul_mul_right {α : Type u} [linear_order α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b c : α) :
max (a * c) (b * c) = (max a b) * c
theorem max_add_add_right {α : Type u} [linear_order α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b c : α) :
max (a + c) (b + c) = max a b + c
theorem min_le_add_of_nonneg_right {α : Type u} [linear_order α] [add_monoid α] [covariant_class α α has_add.add has_le.le] {a b : α} (hb : 0 b) :
min a b a + b
theorem min_le_mul_of_one_le_right {α : Type u} [linear_order α] [monoid α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (hb : 1 b) :
min a b a * b
theorem min_le_add_of_nonneg_left {α : Type u} [linear_order α] [add_monoid α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) :
min a b a + b
theorem min_le_mul_of_one_le_left {α : Type u} [linear_order α] [monoid α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) :
min a b a * b
theorem max_le_mul_of_one_le {α : Type u} [linear_order α] [monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
max a b a * b
theorem max_le_add_of_nonneg {α : Type u} [linear_order α] [add_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
max a b a + b
def function.injective.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback a linear_ordered_cancel_comm_monoid under an injective map. See note [reducible non-instances].

Equations
def function.injective.linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

Pullback a linear_ordered_cancel_add_comm_monoid under an injective map.

Equations
@[protected, instance]
def order_dual.has_add {α : Type u} [h : has_add α] :
Equations
@[protected, instance]
def order_dual.has_mul {α : Type u} [h : has_mul α] :
Equations
@[protected, instance]
def order_dual.has_one {α : Type u} [h : has_one α] :
Equations
@[protected, instance]
def order_dual.add_monoid {α : Type u} [h : add_monoid α] :
Equations
@[protected, instance]
def order_dual.monoid {α : Type u} [h : monoid α] :
Equations
@[protected, instance]
def order_dual.comm_monoid {α : Type u} [h : comm_monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem lt_or_lt_of_add_lt_add {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b m n : α} (h : m + n < a + b) :
m < a n < b
theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} (ha : a ) :
a + b < a + c b < c
theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} (ha : a ) :
c + a < b + a c < b
theorem with_bot.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} (ha : a ) :
a + b < a + c b < c
theorem with_bot.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} (ha : a ) :
b + a < c + a b < c
@[protected, instance]
def multiplicative.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def additive.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.linear_order {α : Type u} [linear_order α] :
Equations
@[simp]
theorem order_embedding.add_left_apply {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α has_add.add has_lt.lt] (m n : α) :
def order_embedding.mul_left {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (m : α) :
α ↪o α

The order embedding sending b to a * b, for some fixed a. See also order_iso.mul_left when working in an ordered group.

Equations
def order_embedding.add_left {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α has_add.add has_lt.lt] (m : α) :
α ↪o α

The order embedding sending b to a + b, for some fixed a. See also order_iso.add_left when working in an additive ordered group.

Equations
@[simp]
theorem order_embedding.mul_left_apply {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (m n : α) :
def order_embedding.mul_right {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (m : α) :
α ↪o α

The order embedding sending b to b * a, for some fixed a. See also order_iso.mul_right when working in an ordered group.

Equations
def order_embedding.add_right {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (m : α) :
α ↪o α

The order embedding sending b to b + a, for some fixed a. See also order_iso.add_right when working in an additive ordered group.

Equations