Pull back ordered groups along injective maps.

@[reducible]

def 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) : OrderedAddCommGroup β

Pullback an OrderedAddCommGroup under an injective map.

Equations

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

theorem Function.Injective.orderedAddCommGroup.proof_6 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (a : β) (b : β) : a + b = b + a

theorem Function.Injective.orderedAddCommGroup.proof_3 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [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) (n : ℕ) (a : β) : SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

theorem Function.Injective.orderedAddCommGroup.proof_5 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [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) (a : β) : -a + a = 0

theorem Function.Injective.orderedAddCommGroup.proof_2 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [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) (a : β) : SubNegMonoid.zsmul 0 a = 0

theorem Function.Injective.orderedAddCommGroup.proof_4 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [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) (n : ℕ) (a : β) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

theorem Function.Injective.orderedAddCommGroup.proof_1 {α : Type u_2} [OrderedAddCommGroup α] {β : Type u_1} [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) (a : β) (b : β) : a - b = a + -b

@[reducible]

def 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) : OrderedCommGroup β

Pullback an OrderedCommGroup under an injective map. See note [reducible non-instances].

Equations

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

@[reducible]

def Function.Injective.linearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_3} [Zero β] [Add β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Sup β] [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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)) : LinearOrderedAddCommGroup β

Pullback a LinearOrderedAddCommGroup under an injective map.

Equations

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

@[reducible]

def Function.Injective.linearOrderedCommGroup {α : Type u_1} [LinearOrderedCommGroup α] {β : Type u_3} [One β] [Mul β] [Inv β] [Div β] [Pow β ℕ] [Pow β ℤ] [Sup β] [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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)) : LinearOrderedCommGroup β

Pullback a LinearOrderedCommGroup under an injective map. See note [reducible non-instances].

Equations

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