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_2) :
Type u_2
  • 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 of this typeclass
Instances of other typeclasses for ordered_comm_monoid
  • ordered_comm_monoid.has_sizeof_inst
@[instance]
@[class]
structure ordered_add_comm_monoid (α : Type u_2) :
Type u_2
  • 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 of this typeclass
Instances of other typeclasses for ordered_add_comm_monoid
  • ordered_add_comm_monoid.has_sizeof_inst
@[class]
structure has_exists_mul_of_le (α : Type u) [has_mul α] [has_le α] :
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 of this typeclass
@[class]
structure has_exists_add_of_le (α : Type u) [has_add α] [has_le α] :
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 of this typeclass
theorem le_of_forall_one_lt_le_mul {α : Type u} [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} (h : ∀ (ε : α), 1 < εa b * ε) :
a b
theorem le_of_forall_pos_le_add {α : Type u} [linear_order α] [densely_ordered α] [add_monoid α] [has_exists_add_of_le α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} (h : ∀ (ε : α), 0 < εa b + ε) :
a b
theorem le_of_forall_pos_lt_add' {α : Type u} [linear_order α] [densely_ordered α] [add_monoid α] [has_exists_add_of_le α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
a b
theorem le_of_forall_one_lt_lt_mul' {α : Type u} [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
a b
theorem le_iff_forall_pos_lt_add' {α : Type u} [linear_order α] [densely_ordered α] [add_monoid α] [has_exists_add_of_le α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} :
a b ∀ (ε : α), 0 < εa < b + ε
theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a b ∀ (ε : α), 1 < εa < b * ε
@[class]
structure linear_ordered_add_comm_monoid (α : Type u_2) :
Type u_2

A linearly ordered additive commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid
  • linear_ordered_add_comm_monoid.has_sizeof_inst
@[class]
structure linear_ordered_comm_monoid (α : Type u_2) :
Type u_2

A linearly ordered commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_monoid
  • linear_ordered_comm_monoid.has_sizeof_inst
@[class]
structure zero_le_one_class (α : Type u_2) [has_zero α] [has_one α] [has_le α] :
Type
  • zero_le_one : 0 1

Typeclass for expressing that the 0 of a type is less or equal to its 1.

Instances of this typeclass
Instances of other typeclasses for zero_le_one_class
  • zero_le_one_class.has_sizeof_inst
@[simp]
theorem zero_le_one {α : Type u} [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
0 1
theorem zero_le_one' (α : Type u_1) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
0 1
theorem zero_le_two {α : Type u} [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α] [covariant_class α α has_add.add has_le.le] :
0 2
theorem zero_le_four {α : Type u} [preorder α] [has_one α] [add_zero_class α] [zero_le_one_class α] [covariant_class α α has_add.add has_le.le] :
0 4
theorem one_le_two {α : Type u} [has_le α] [has_one α] [add_zero_class α] [zero_le_one_class α] [covariant_class α α has_add.add has_le.le] :
1 2
@[class]
structure linear_ordered_comm_monoid_with_zero (α : Type u_2) :
Type u_2

A linearly ordered commutative monoid with a zero element.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_monoid_with_zero
  • linear_ordered_comm_monoid_with_zero.has_sizeof_inst
@[class]
structure linear_ordered_add_comm_monoid_with_top (α : Type u_2) :
Type u_2

A linearly ordered commutative monoid with an additively absorbing element. Instances should include number systems with an infinite element adjoined.`

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid_with_top
  • linear_ordered_add_comm_monoid_with_top.has_sizeof_inst
@[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 : α) :
@[reducible]
def function.injective.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] [has_pow β ] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

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

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

Pullback an ordered_add_comm_monoid under an injective map.

Equations
@[reducible]
def function.injective.linear_ordered_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] [has_pow β ] [has_sup β] [has_inf β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : ∀ (x y : β), f (x y) = linear_order.max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = linear_order.min (f x) (f y)) :

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

Equations
@[reducible]
def function.injective.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] [has_smul β] [has_sup β] [has_inf β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (hsup : ∀ (x y : β), f (x y) = linear_order.max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = linear_order.min (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 : αˣ} :
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 : αˣ} :
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
def units.order_embedding_coe {α : Type u} [monoid α] [linear_order α] :
αˣ ↪o α

coe : αˣ → α as an order embedding.

Equations
def add_units.order_embedding_coe {α : Type u} [add_monoid α] [linear_order α] :

coe : add_units α → α as an order embedding.

Equations
@[simp, norm_cast]
theorem add_units.max_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
@[simp, norm_cast]
theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : αˣ} :
@[simp, norm_cast]
theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : αˣ} :
@[simp, norm_cast]
theorem add_units.min_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
@[protected, instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_zero.order_bot {α : Type u} [preorder α] :
Equations
theorem with_zero.zero_le {α : Type u} [preorder α] (a : with_zero α) :
0 a
theorem with_zero.zero_lt_coe {α : Type u} [preorder α] (a : α) :
0 < a
theorem with_zero.zero_eq_bot {α : Type u} [preorder α] :
0 =
@[simp, norm_cast]
theorem with_zero.coe_lt_coe {α : Type u} [preorder α] {a b : α} :
a < b a < b
@[simp, norm_cast]
theorem with_zero.coe_le_coe {α : Type u} [preorder α] {a b : α} :
a b a b
@[protected, instance]
def with_zero.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem with_zero.le_max_iff {α : Type u} [linear_order α] {a b c : α} :
@[simp]
theorem with_zero.min_le_iff {α : Type u} [linear_order α] {a b c : α} :
@[protected]
@[class]
structure canonically_ordered_add_monoid (α : Type u_2) :
Type u_2
  • 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 : α), canonically_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), canonically_ordered_add_monoid.nsmul n.succ x = x + canonically_ordered_add_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
  • bot : α
  • bot_le : ∀ (x : α), x
  • exists_add_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a + c)
  • le_self_add : ∀ (a b : α), a a + b

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 of this typeclass
Instances of other typeclasses for canonically_ordered_add_monoid
  • canonically_ordered_add_monoid.has_sizeof_inst
@[instance]
@[class]
structure canonically_ordered_monoid (α : Type u_2) :
Type u_2
  • 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
  • exists_mul_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a * c)
  • le_self_mul : ∀ (a b : α), a a * b

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 of this typeclass
Instances of other typeclasses for canonically_ordered_monoid
  • canonically_ordered_monoid.has_sizeof_inst
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 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 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
theorem le_of_mul_le_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} :
a * b ca c
theorem le_of_add_le_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a + b ca c
theorem le_of_add_le_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a + b cb c
theorem le_of_mul_le_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} :
a * b cb c
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 le_iff_exists_add' {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b ∃ (c : α), b = c + a
theorem le_iff_exists_mul' {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b ∃ (c : α), b = c * 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
theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :
= 1
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 eq_zero_or_pos {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
a = 0 0 < a
theorem eq_one_or_one_lt {α : Type u} [canonically_ordered_monoid α] {a : α} :
a = 1 1 < a
@[simp]
theorem one_lt_mul_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :
1 < a * b 1 < a 1 < b
@[simp]
theorem add_pos_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
0 < a + b 0 < a 0 < b
theorem exists_one_lt_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :
∃ (c : α) (hc : 1 < c), a * c = b
theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :
∃ (c : α) (hc : 0 < c), 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_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 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
@[protected, instance]
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_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for canonically_linear_ordered_add_monoid
  • canonically_linear_ordered_add_monoid.has_sizeof_inst
@[class]
structure canonically_linear_ordered_monoid (α : Type u_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for canonically_linear_ordered_monoid
  • canonically_linear_ordered_monoid.has_sizeof_inst
@[simp]
theorem one_min {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
@[simp]
theorem zero_min {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
@[simp]
theorem min_zero {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
@[simp]
theorem min_one {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
@[simp]
theorem bot_eq_one' {α : Type u} [canonically_linear_ordered_monoid α] :
= 1

In a linearly ordered monoid, we are happy for bot_eq_one to be a @[simp] lemma.

@[simp]
theorem bot_eq_zero' {α : Type u} [canonically_linear_ordered_add_monoid α] :
= 0

In a linearly ordered monoid, we are happy for bot_eq_zero to be a @[simp] lemma

@[class]
structure ordered_cancel_add_comm_monoid (α : Type u) :
Type u

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

Instances of this typeclass
Instances of other typeclasses for ordered_cancel_add_comm_monoid
  • ordered_cancel_add_comm_monoid.has_sizeof_inst
@[class]
structure ordered_cancel_comm_monoid (α : Type u) :
Type u
  • 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_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 of this typeclass
Instances of other typeclasses for ordered_cancel_comm_monoid
  • ordered_cancel_comm_monoid.has_sizeof_inst
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
@[reducible]
def function.injective.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] [has_pow β ] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

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

Equations

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 (linear_order.min n m) * f (linear_order.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 (linear_order.min n m) + f (linear_order.max n m) = f n + f m
theorem min_add_max {α : Type u} [linear_order α] [add_comm_semigroup α] (n m : α) :
theorem min_mul_max {α : Type u} [linear_order α] [comm_semigroup α] (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 of this typeclass
Instances of other typeclasses for linear_ordered_cancel_add_comm_monoid
  • linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for linear_ordered_cancel_comm_monoid
  • linear_ordered_cancel_comm_monoid.has_sizeof_inst
theorem min_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
theorem min_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
theorem max_add_add_left {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a b c : α) :
theorem max_mul_mul_left {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (a b c : α) :
theorem lt_or_lt_of_add_lt_add {α : Type u} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b m n : α} (h : m + n < a + b) :
m < a n < b
theorem lt_or_lt_of_mul_lt_mul {α : Type u} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b m n : α} (h : m * n < a * b) :
m < a n < b
theorem min_add_add_right {α : Type u} [linear_order α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (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 : α) :
theorem max_mul_mul_right {α : Type u} [linear_order α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (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 : α) :
theorem min_le_add_of_nonneg_right {α : Type u} [linear_order α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (hb : 0 b) :
theorem min_le_mul_of_one_le_right {α : Type u} [linear_order α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (hb : 1 b) :
theorem min_le_add_of_nonneg_left {α : Type u} [linear_order α] [add_zero_class α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) :
theorem min_le_mul_of_one_le_left {α : Type u} [linear_order α] [mul_one_class α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) :
theorem max_le_mul_of_one_le {α : Type u} [linear_order α] [mul_one_class α] [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) :
theorem max_le_add_of_nonneg {α : Type u} [linear_order α] [add_zero_class α] [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) :
@[reducible]
def function.injective.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] [has_pow β ] [has_sup β] [has_inf β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : ∀ (x y : β), f (x y) = linear_order.max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = linear_order.min (f x) (f y)) :

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

Equations
@[reducible]
def function.injective.linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] [has_smul β] [has_sup β] [has_inf β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (hsup : ∀ (x y : β), f (x y) = linear_order.max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = linear_order.min (f x) (f y)) :

Pullback a linear_ordered_cancel_add_comm_monoid under an injective map.

Equations

Order dual #

Product #

@[protected, instance]
def prod.has_exists_add_of_le {α : Type u} {β : Type u_1} [has_le α] [has_le β] [has_add α] [has_add β] [has_exists_add_of_le α] [has_exists_add_of_le β] :
@[protected, instance]
def prod.has_exists_mul_of_le {α : Type u} {β : Type u_1} [has_le α] [has_le β] [has_mul α] [has_mul β] [has_exists_mul_of_le α] [has_exists_mul_of_le β] :

with_bot/with_top #

@[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
@[protected, simp]
theorem with_top.map_zero {α : Type u} [has_zero α] {β : Type u_1} (f : α → β) :
with_top.map f 0 = (f 0)
@[protected, simp]
theorem with_top.map_one {α : Type u} [has_one α] {β : Type u_1} (f : α → β) :
with_top.map f 1 = (f 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]
Equations
@[protected, instance]
def with_top.has_add {α : Type u} [has_add α] :
Equations
@[norm_cast]
theorem with_top.coe_add {α : Type u} [has_add α] {x y : α} :
(x + y) = x + y
@[norm_cast]
theorem with_top.coe_bit0 {α : Type u} [has_add α] {x : α} :
@[norm_cast]
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
@[simp]
theorem with_top.top_add {α : Type u} [has_add α] (a : with_top α) :
@[simp]
theorem with_top.add_top {α : Type u} [has_add α] (a : with_top α) :
@[simp]
theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :
a + b = a = b =
theorem with_top.add_ne_top {α : Type u} [has_add α] {a b : with_top α} :
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]
theorem with_top.le_of_add_le_add_left {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [contravariant_class α α has_add.add has_le.le] (ha : a ) (h : a + b a + c) :
b c
@[protected]
theorem with_top.le_of_add_le_add_right {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [contravariant_class α α (function.swap has_add.add) has_le.le] (ha : a ) (h : b + a c + a) :
b c
@[protected]
theorem with_top.add_lt_add_left {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α has_add.add has_lt.lt] (ha : a ) (h : b < c) :
a + b < a + c
@[protected]
theorem with_top.add_lt_add_right {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ) (h : b < c) :
b + a < c + a
@[protected]
theorem with_top.add_le_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (ha : a ) :
a + b a + c b c
@[protected]
@[protected]
theorem with_top.add_lt_add_iff_left {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (ha : a ) :
a + b < a + c b < c
@[protected]
theorem with_top.add_lt_add_iff_right {α : Type u} [has_add α] {a b c : with_top α} [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (ha : a ) :
b + a < c + a b < c
@[protected]
theorem with_top.add_lt_add_of_le_of_lt {α : Type u} [has_add α] {a b c d : with_top α} [preorder α] [covariant_class α α has_add.add