Pulling back ordered rings along injective maps.

ink

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) : OrderedSemiring β

Pullback an OrderedSemiring under an injective map.

Equations

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

ink

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) : OrderedCommSemiring β

Pullback an OrderedCommSemiring under an injective map.

Equations

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

ink

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) : OrderedRing β

Pullback an OrderedRing under an injective map.

Equations

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

ink

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) : OrderedCommRing β

Pullback an OrderedCommRing under an injective map.

Equations

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

ink

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) : StrictOrderedSemiring β

Pullback a StrictOrderedSemiring under an injective map.

Equations

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

ink

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) : StrictOrderedCommSemiring β

Pullback a strictOrderedCommSemiring under an injective map.

Equations

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

ink

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) : StrictOrderedRing β

Pullback a StrictOrderedRing under an injective map.

Equations

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

ink

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) : StrictOrderedCommRing β

Pullback a StrictOrderedCommRing under an injective map.

Equations

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

ink

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)) : LinearOrderedSemiring β

Pullback a LinearOrderedSemiring under an injective map.

Equations

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

ink

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)) : LinearOrderedCommSemiring β

Pullback a LinearOrderedSemiring under an injective map.

Equations

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

ink

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)) : LinearOrderedRing β

Pullback a LinearOrderedRing under an injective map.

Equations

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

ink

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)) : LinearOrderedCommRing β

Pullback a LinearOrderedCommRing under an injective map.

Equations

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