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}
[ordered_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast = {add := ordered_add_comm_monoid.add (function.injective.ordered_add_comm_monoid f hf zero add nsmul), add_assoc := _, zero := ordered_add_comm_monoid.zero (function.injective.ordered_add_comm_monoid f hf zero add nsmul), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (function.injective.ordered_add_comm_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (function.injective.semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, le := ordered_add_comm_monoid.le (function.injective.ordered_add_comm_monoid f hf zero add nsmul), lt := ordered_add_comm_monoid.lt (function.injective.ordered_add_comm_monoid f hf zero add nsmul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _}
@[protected, reducible]
def
function.injective.ordered_comm_semiring
{α : Type u}
{β : Type u_1}
[ordered_comm_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.ordered_comm_semiring f hf zero one add mul nsmul npow nat_cast = {add := comm_semiring.add (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := comm_semiring.zero (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, le := ordered_semiring.le (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), lt := ordered_semiring.lt (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}
@[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_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[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
- function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := ordered_semiring.add (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := ordered_semiring.zero (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := ordered_semiring.nsmul (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ring.zsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := ordered_semiring.nat_cast (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), one := ordered_semiring.one (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ordered_semiring.mul (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := ordered_semiring.npow (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_semiring.le (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), lt := ordered_semiring.lt (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _}
@[protected, reducible]
def
function.injective.ordered_comm_ring
{α : Type u}
{β : Type u_1}
[ordered_comm_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_smul ℤ β]
[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
- function.injective.ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := ordered_ring.add (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := ordered_ring.zero (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ordered_ring.sub (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ordered_ring.zsmul (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ordered_ring.int_cast (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := ordered_ring.nat_cast (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := ordered_ring.one (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ordered_ring.mul (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := ordered_ring.npow (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_ring.le (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), lt := ordered_ring.lt (function.injective.ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_nonneg := _, mul_comm := _}
@[protected, reducible]
def
function.injective.strict_ordered_semiring
{α : Type u}
{β : Type u_1}
[strict_ordered_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast = {add := ordered_cancel_add_comm_monoid.add (function.injective.ordered_cancel_add_comm_monoid f hf zero add nsmul), add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero (function.injective.ordered_cancel_add_comm_monoid f hf zero add nsmul), zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul (function.injective.ordered_cancel_add_comm_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ordered_semiring.mul (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ordered_semiring.one (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := ordered_semiring.nat_cast (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := ordered_semiring.npow (function.injective.ordered_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, le := ordered_cancel_add_comm_monoid.le (function.injective.ordered_cancel_add_comm_monoid f hf zero add nsmul), lt := ordered_cancel_add_comm_monoid.lt (function.injective.ordered_cancel_add_comm_monoid f hf zero add nsmul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}
@[protected, reducible]
def
function.injective.strict_ordered_comm_semiring
{α : Type u}
{β : Type u_1}
[strict_ordered_comm_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.strict_ordered_comm_semiring f hf zero one add mul nsmul npow nat_cast = {add := comm_semiring.add (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := comm_semiring.zero (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow (function.injective.comm_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, le := strict_ordered_semiring.le (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), lt := strict_ordered_semiring.lt (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _}
@[protected, reducible]
def
function.injective.strict_ordered_ring
{α : Type u}
{β : Type u_1}
[strict_ordered_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[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
- function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := strict_ordered_semiring.add (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := strict_ordered_semiring.zero (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := strict_ordered_semiring.nsmul (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := ring.zsmul (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (function.injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := strict_ordered_semiring.nat_cast (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), one := strict_ordered_semiring.one (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_semiring.mul (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_semiring.npow (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_semiring.le (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), lt := strict_ordered_semiring.lt (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _}
@[protected, reducible]
def
function.injective.strict_ordered_comm_ring
{α : Type u}
{β : Type u_1}
[strict_ordered_comm_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_smul ℤ β]
[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
- function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast = {add := strict_ordered_ring.add (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := strict_ordered_ring.zero (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := strict_ordered_ring.sub (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := strict_ordered_ring.nat_cast (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := strict_ordered_ring.one (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), lt := strict_ordered_ring.lt (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, mul_comm := _}
@[protected, reducible]
def
function.injective.linear_ordered_semiring
{α : Type u}
{β : Type u_1}
[linear_ordered_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf = {add := strict_ordered_semiring.add (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), add_assoc := _, zero := strict_ordered_semiring.zero (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), zero_add := _, add_zero := _, nsmul := strict_ordered_semiring.nsmul (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := strict_ordered_semiring.mul (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := strict_ordered_semiring.one (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), one_mul := _, mul_one := _, nat_cast := strict_ordered_semiring.nat_cast (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), nat_cast_zero := _, nat_cast_succ := _, npow := strict_ordered_semiring.npow (function.injective.strict_ordered_semiring f hf zero one add mul nsmul npow nat_cast), npow_zero' := _, npow_succ' := _, le := linear_order.le (linear_order.lift f hf hsup hinf), lt := linear_order.lt (linear_order.lift f hf hsup hinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf hsup hinf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf hsup hinf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf hsup hinf), max := linear_order.max (linear_order.lift f hf hsup hinf), max_def := _, min := linear_order.min (linear_order.lift f hf hsup hinf), min_def := _}
@[protected, reducible]
def
function.injective.linear_ordered_comm_semiring
{α : Type u}
{β : Type u_1}
[linear_ordered_comm_semiring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[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
- function.injective.linear_ordered_comm_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf = {add := linear_ordered_semiring.add (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), add_assoc := _, zero := linear_ordered_semiring.zero (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), zero_add := _, add_zero := _, nsmul := linear_ordered_semiring.nsmul (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := linear_ordered_semiring.mul (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := linear_ordered_semiring.one (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), one_mul := _, mul_one := _, nat_cast := linear_ordered_semiring.nat_cast (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), nat_cast_zero := _, nat_cast_succ := _, npow := linear_ordered_semiring.npow (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), npow_zero' := _, npow_succ' := _, le := linear_ordered_semiring.le (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), lt := linear_ordered_semiring.lt (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, mul_comm := _, le_total := _, decidable_le := linear_ordered_semiring.decidable_le (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), decidable_eq := linear_ordered_semiring.decidable_eq (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), decidable_lt := linear_ordered_semiring.decidable_lt (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), max := linear_ordered_semiring.max (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), max_def := _, min := linear_ordered_semiring.min (function.injective.linear_ordered_semiring f hf zero one add mul nsmul npow nat_cast hsup hinf), min_def := _}
@[reducible]
def
function.injective.linear_ordered_ring
{α : Type u}
{β : Type u_1}
[linear_ordered_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_pow β ℕ]
[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
- function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf = {add := strict_ordered_ring.add (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := strict_ordered_ring.zero (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := strict_ordered_ring.sub (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := strict_ordered_ring.nat_cast (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := strict_ordered_ring.one (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow (function.injective.strict_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le (linear_order.lift f hf hsup hinf), lt := linear_order.lt (linear_order.lift f hf hsup hinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf hsup hinf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf hsup hinf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf hsup hinf), max := linear_order.max (linear_order.lift f hf hsup hinf), max_def := _, min := linear_order.min (linear_order.lift f hf hsup hinf), min_def := _}
@[protected, reducible]
def
function.injective.linear_ordered_comm_ring
{α : Type u}
{β : Type u_1}
[linear_ordered_comm_ring α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_smul ℤ β]
[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
- function.injective.linear_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf = {add := strict_ordered_comm_ring.add (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), add_assoc := _, zero := strict_ordered_comm_ring.zero (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zero_add := _, add_zero := _, nsmul := strict_ordered_comm_ring.nsmul (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_comm_ring.neg (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub := strict_ordered_comm_ring.sub (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), sub_eq_add_neg := _, zsmul := strict_ordered_comm_ring.zsmul (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_comm_ring.int_cast (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast := strict_ordered_comm_ring.nat_cast (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), one := strict_ordered_comm_ring.one (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_comm_ring.mul (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_comm_ring.npow (function.injective.strict_ordered_comm_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le (linear_order.lift f hf hsup hinf), lt := linear_order.lt (linear_order.lift f hf hsup hinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf hsup hinf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf hsup hinf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf hsup hinf), max := linear_order.max (linear_order.lift f hf hsup hinf), max_def := _, min := linear_order.min (linear_order.lift f hf hsup hinf), min_def := _, mul_comm := _}