# mathlib3documentation

algebra.order.monoid.basic

# Ordered monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops some additional material on ordered monoids.

@[reducible]
def function.injective.ordered_comm_monoid {α : Type u} {β : 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) (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} {β : 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) (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} {β : Type u_1} [has_one β] [has_mul β] [ ] [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} {β : Type u_1} [has_zero β] [has_add β] [ β] [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
@[simp]
theorem order_embedding.add_left_apply {α : Type u_1} [has_add α] [linear_order α] (m n : α) :
= m + n
def order_embedding.mul_left {α : Type u_1} [has_mul α] [linear_order α] (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 α] (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 α] (m n : α) :
= m * n
@[simp]
theorem order_embedding.mul_right_apply {α : Type u_1} [has_mul α] [linear_order α] (m n : α) :
= n * m
def order_embedding.mul_right {α : Type u_1} [has_mul α] [linear_order α] (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
@[simp]
theorem order_embedding.add_right_apply {α : Type u_1} [has_add α] [linear_order α] (m n : α) :
= n + m
def order_embedding.add_right {α : Type u_1} [has_add α] [linear_order α] (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