# Documentation

Mathlib.Algebra.Order.Ring.InjSurj

# Pulling back ordered rings along injective maps. #

@[reducible]
def Function.Injective.orderedSemiring {α : Type u} {β : Type u_1} [] [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] (f : βα) (hf : ) (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 OrderedSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.orderedCommSemiring {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] (f : βα) (hf : ) (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 OrderedCommSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.orderedRing {α : Type u} {β : Type u_1} [] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [] [] [Pow β ] [] [] (f : βα) (hf : ) (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 OrderedRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.orderedCommRing {α : Type u} {β : Type u_1} [] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [Pow β ] [] [] [] [] (f : βα) (hf : ) (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 OrderedCommRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.strictOrderedSemiring {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] (f : βα) (hf : ) (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 StrictOrderedSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.strictOrderedCommSemiring {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] (f : βα) (hf : ) (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 strictOrderedCommSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.strictOrderedRing {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [] [] [Pow β ] [] [] (f : βα) (hf : ) (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 StrictOrderedRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.strictOrderedCommRing {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [Pow β ] [] [] [] [] (f : βα) (hf : ) (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 StrictOrderedCommRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedSemiring {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] [Sup β] [Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedCommSemiring {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [] [] [Sup β] [Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedSemiring under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedRing {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [] [] [Pow β ] [] [] [Sup β] [Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible]
def Function.Injective.linearOrderedCommRing {α : Type u} {β : Type u_1} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [Pow β ] [] [] [] [] [Sup β] [Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

Pullback a LinearOrderedCommRing under an injective map.

Equations
• One or more equations did not get rendered due to their size.
Instances For