Pulling back ordered rings along injective maps. #
def
Function.Injective.orderedSemiring
{α : Type u}
{β : Type u_1}
[inst : OrderedSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
(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 OrderedSemiring
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.orderedCommSemiring
{α : Type u}
{β : Type u_1}
[inst : OrderedCommSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
(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 OrderedCommSemiring
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.orderedRing
{α : Type u}
{β : Type u_1}
[inst : OrderedRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : Pow β ℕ]
[inst : NatCast β]
[inst : IntCast β]
(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 OrderedRing
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.orderedCommRing
{α : Type u}
{β : Type u_1}
[inst : OrderedCommRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : NatCast β]
[inst : IntCast β]
(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 OrderedCommRing
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.strictOrderedSemiring
{α : Type u}
{β : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
(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 StrictOrderedSemiring
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.strictOrderedCommSemiring
{α : Type u}
{β : Type u_1}
[inst : StrictOrderedCommSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
(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 strictOrderedCommSemiring
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.strictOrderedRing
{α : Type u}
{β : Type u_1}
[inst : StrictOrderedRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : Pow β ℕ]
[inst : NatCast β]
[inst : IntCast β]
(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 StrictOrderedRing
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.strictOrderedCommRing
{α : Type u}
{β : Type u_1}
[inst : StrictOrderedCommRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : NatCast β]
[inst : IntCast β]
(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 StrictOrderedCommRing
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
def
Function.Injective.linearOrderedSemiring
{α : Type u}
{β : Type u_1}
[inst : LinearOrderedSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
[inst : Sup β]
[inst : 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) = 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.
def
Function.Injective.linearOrderedCommSemiring
{α : Type u}
{β : Type u_1}
[inst : LinearOrderedCommSemiring α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : NatCast β]
[inst : Sup β]
[inst : 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) = 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.
def
Function.Injective.linearOrderedRing
{α : Type u}
{β : Type u_1}
[inst : LinearOrderedRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : Pow β ℕ]
[inst : NatCast β]
[inst : IntCast β]
[inst : Sup β]
[inst : 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) = 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.
def
Function.Injective.linearOrderedCommRing
{α : Type u}
{β : Type u_1}
[inst : LinearOrderedCommRing α]
[inst : Zero β]
[inst : One β]
[inst : Add β]
[inst : Mul β]
[inst : Neg β]
[inst : Sub β]
[inst : Pow β ℕ]
[inst : SMul ℕ β]
[inst : SMul ℤ β]
[inst : NatCast β]
[inst : IntCast β]
[inst : Sup β]
[inst : 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) = 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.