Pulling back linearly ordered fields along injective maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[reducible]
def
function.injective.linear_ordered_semifield
{α : Type u_2}
{β : Type u_3}
[linear_ordered_semifield α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_nat_cast β]
[has_inv β]
[has_div β]
[has_pow β ℤ]
[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)
(inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹)
(div : ∀ (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)
(zpow : ∀ (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_semifield under an injective map.
Equations
- function.injective.linear_ordered_semifield f hf zero one add mul inv div nsmul npow zpow 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 := _, inv := semifield.inv (function.injective.semifield f hf zero one add mul inv div nsmul npow zpow nat_cast), div := semifield.div (function.injective.semifield f hf zero one add mul inv div nsmul npow zpow nat_cast), div_eq_mul_inv := _, zpow := semifield.zpow (function.injective.semifield f hf zero one add mul inv div nsmul npow zpow nat_cast), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_zero := _, mul_inv_cancel := _}
@[reducible]
def
function.injective.linear_ordered_field
{α : Type u_2}
{β : Type u_3}
[linear_ordered_field α]
[has_zero β]
[has_one β]
[has_add β]
[has_mul β]
[has_neg β]
[has_sub β]
[has_pow β ℕ]
[has_smul ℕ β]
[has_smul ℤ β]
[has_smul ℚ β]
[has_nat_cast β]
[has_int_cast β]
[has_rat_cast β]
[has_inv β]
[has_div β]
[has_pow β ℤ]
[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)
(inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹)
(div : ∀ (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)
(qsmul : ∀ (x : β) (n : ℚ), f (n • x) = n • f x)
(npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
(int_cast : ∀ (n : ℤ), f ↑n = ↑n)
(rat_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_field under an injective map.
Equations
- function.injective.linear_ordered_field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast hsup hinf = {add := linear_ordered_ring.add (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), add_assoc := _, zero := linear_ordered_ring.zero (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), sub := linear_ordered_ring.sub (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_ring.int_cast (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), nat_cast := linear_ordered_ring.nat_cast (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), one := linear_ordered_ring.one (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_ring.mul (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), lt := linear_ordered_ring.lt (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast 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_ordered_ring.decidable_le (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), decidable_eq := linear_ordered_ring.decidable_eq (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), decidable_lt := linear_ordered_ring.decidable_lt (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), max := linear_ordered_ring.max (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), max_def := _, min := linear_ordered_ring.min (function.injective.linear_ordered_ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast hsup hinf), min_def := _, mul_comm := _, inv := field.inv (function.injective.field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast), div := field.div (function.injective.field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast), div_eq_mul_inv := _, zpow := field.zpow (function.injective.field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, rat_cast := field.rat_cast (function.injective.field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul (function.injective.field f hf zero one add mul neg sub inv div nsmul zsmul qsmul npow zpow nat_cast int_cast rat_cast), qsmul_eq_mul' := _}