# mathlib3documentation

algebra.order.ring.inj_surj

# Pulling back ordered rings along injective maps. #

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

@[protected, reducible]
def function.injective.ordered_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback an ordered_semiring under an injective map.

Equations
@[protected, reducible]
def function.injective.ordered_comm_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback an ordered_comm_semiring under an injective map.

Equations
@[protected, reducible]
def function.injective.ordered_ring {α : Type u} {β : Type u_1} [ordered_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback an ordered_ring under an injective map.

Equations
@[protected, reducible]
def function.injective.ordered_comm_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ ] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback an ordered_comm_ring under an injective map.

Equations
@[protected, reducible]
def function.injective.strict_ordered_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a strict_ordered_semiring under an injective map.

Equations
@[protected, reducible]
def function.injective.strict_ordered_comm_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) :

Pullback a strict_ordered_comm_semiring under an injective map.

Equations
@[protected, reducible]
def function.injective.strict_ordered_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback a strict_ordered_ring under an injective map.

Equations
@[protected, reducible]
def function.injective.strict_ordered_comm_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ ] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = n) :

Pullback a strict_ordered_comm_ring under an injective map.

Equations
@[protected, reducible]
def function.injective.linear_ordered_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] [has_sup β] [has_inf β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = 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_semiring under an injective map.

Equations
@[protected, reducible]
def function.injective.linear_ordered_comm_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] [has_sup β] [has_inf β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = 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_semiring under an injective map.

Equations
@[reducible]
def function.injective.linear_ordered_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] [has_sup β] [has_inf β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = 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_ring under an injective map.

Equations
@[protected, reducible]
def function.injective.linear_ordered_comm_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ ] [ β] [ β] [has_nat_cast β] [has_int_cast β] [has_sup β] [has_inf β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : (x y : β), f (x + y) = f x + f y) (mul : (x y : β), f (x * y) = f x * f y) (neg : (x : β), f (-x) = -f x) (sub : (x y : β), f (x - y) = f x - f y) (nsmul : (x : β) (n : ), f (n x) = n f x) (zsmul : (x : β) (n : ), f (n x) = n f x) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : (n : ), f n = n) (int_cast : (n : ), f n = 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_ring under an injective map.

Equations