Pull back ordered groups along injective maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[reducible]
def
function.injective.ordered_add_comm_group
{α : Type u_1}
[ordered_add_comm_group α]
{β : Type u_2}
[has_zero β]
[has_add β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(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)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
Pullback an ordered_add_comm_group under an injective map.
Equations
- function.injective.ordered_add_comm_group f hf one mul inv div npow zpow = {add := ordered_add_comm_monoid.add (function.injective.ordered_add_comm_monoid f hf one mul npow), add_assoc := _, zero := ordered_add_comm_monoid.zero (function.injective.ordered_add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (function.injective.ordered_add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf one mul inv div npow zpow), sub := add_comm_group.sub (function.injective.add_comm_group f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (function.injective.add_comm_group f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[reducible]
def
function.injective.ordered_comm_group
{α : Type u_1}
[ordered_comm_group α]
{β : Type u_2}
[has_one β]
[has_mul β]
[has_inv β]
[has_div β]
[has_pow β ℕ]
[has_pow β ℤ]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(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)
(npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n) :
Pullback an ordered_comm_group under an injective map.
See note [reducible non-instances].
Equations
- function.injective.ordered_comm_group f hf one mul inv div npow zpow = {mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul npow), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, inv := comm_group.inv (function.injective.comm_group f hf one mul inv div npow zpow), div := comm_group.div (function.injective.comm_group f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := comm_group.zpow (function.injective.comm_group f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}
@[reducible]
def
function.injective.linear_ordered_comm_group
{α : Type u_1}
[linear_ordered_comm_group α]
{β : Type u_2}
[has_one β]
[has_mul β]
[has_inv β]
[has_div β]
[has_pow β ℕ]
[has_pow β ℤ]
[has_sup β]
[has_inf β]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(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)
(npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ 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_group under an injective map.
See note [reducible non-instances].
Equations
- function.injective.linear_ordered_comm_group f hf one mul inv div npow zpow hsup hinf = {mul := ordered_comm_group.mul (function.injective.ordered_comm_group f hf one mul inv div npow zpow), mul_assoc := _, one := ordered_comm_group.one (function.injective.ordered_comm_group f hf one mul inv div npow zpow), one_mul := _, mul_one := _, npow := ordered_comm_group.npow (function.injective.ordered_comm_group f hf one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv (function.injective.ordered_comm_group f hf one mul inv div npow zpow), div := ordered_comm_group.div (function.injective.ordered_comm_group f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := ordered_comm_group.zpow (function.injective.ordered_comm_group f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, 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 := _, mul_le_mul_left := _, 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 := _}
@[reducible]
def
function.injective.linear_ordered_add_comm_group
{α : Type u_1}
[linear_ordered_add_comm_group α]
{β : Type u_2}
[has_zero β]
[has_add β]
[has_neg β]
[has_sub β]
[has_smul ℕ β]
[has_smul ℤ β]
[has_sup β]
[has_inf β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(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)
(npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : β) (n : ℤ), f (n • x) = n • f x)
(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_add_comm_group under an injective map.
Equations
- function.injective.linear_ordered_add_comm_group f hf one mul inv div npow zpow hsup hinf = {add := ordered_add_comm_group.add (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), add_assoc := _, zero := ordered_add_comm_group.zero (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), sub := ordered_add_comm_group.sub (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul (function.injective.ordered_add_comm_group f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, 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_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 := _}