Pull back ordered groups along injective maps. #
@[reducible, inline]
abbrev
Function.Injective.orderedCommGroup
{α : Type u_1}
[OrderedCommGroup α]
{β : Type u_3}
[One β]
[Mul β]
[Inv β]
[Div β]
[Pow β ℕ]
[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 OrderedCommGroup under an injective map.
See note [reducible non-instances].
Equations
- Function.Injective.orderedCommGroup f hf one mul inv div npow zpow = OrderedCommGroup.mk ⋯
Instances For
@[reducible, inline]
abbrev
Function.Injective.orderedAddCommGroup
{α : Type u_1}
[OrderedAddCommGroup α]
{β : Type u_3}
[Zero β]
[Add β]
[Neg β]
[Sub β]
[SMul ℕ β]
[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 OrderedAddCommGroup under an injective map.
Equations
- Function.Injective.orderedAddCommGroup f hf one mul inv div npow zpow = OrderedAddCommGroup.mk ⋯
Instances For
@[reducible, inline]
abbrev
Function.Injective.linearOrderedCommGroup
{α : Type u_1}
[LinearOrderedCommGroup α]
{β : Type u_3}
[One β]
[Mul β]
[Inv β]
[Div β]
[Pow β ℕ]
[Pow β ℤ]
[Max β]
[Min β]
(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)
(sup : ∀ (x y : β), f (x ⊔ y) = f x ⊔ f y)
(inf : ∀ (x y : β), f (x ⊓ y) = f x ⊓ f y)
:
Pullback a LinearOrderedCommGroup under an injective map.
See note [reducible non-instances].
Equations
- Function.Injective.linearOrderedCommGroup f hf one mul inv div npow zpow sup inf = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
Function.Injective.linearOrderedAddCommGroup
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{β : Type u_3}
[Zero β]
[Add β]
[Neg β]
[Sub β]
[SMul ℕ β]
[SMul ℤ β]
[Max β]
[Min β]
(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)
(sup : ∀ (x y : β), f (x ⊔ y) = f x ⊔ f y)
(inf : ∀ (x y : β), f (x ⊓ y) = f x ⊓ f y)
:
Pullback a LinearOrderedAddCommGroup under an injective map.
Equations
- Function.Injective.linearOrderedAddCommGroup f hf one mul inv div npow zpow sup inf = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯