Lifting algebraic data classes along injective/surjective maps

This file provides definitions that are meant to deal with situations such as the following:

Suppose that G is a group, and H is a type endowed with One H, Mul H, and Inv H. Suppose furthermore, that f : G → H→ H is a surjective map that respects the multiplication, and the unit elements. Then H satisfies the group axioms.

The relevant definition in this case is Function.Surjective.group. Dually, there is also Function.Injective.group. And there are versions for (additive) (commutative) semigroups/monoids.

Injective

ink

def Function.Injective.addSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) : x + y + z = x + (y + z)

Equations

• (_ : x + y + z = x + (y + z)) = hf (x + y + z) (x + (y + z)) (_ : f (x + y + z) = f (x + (y + z)))

ink

def Function.Injective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddSemigroup M₁

A type endowed with + is an additive semigroup, if it admits an injective map that preserves + to an additive semigroup.

Equations

• Function.Injective.addSemigroup f hf mul = let src := inst; AddSemigroup.mk (_ : ∀ (x y z : M₁), x + y + z = x + (y + z))

ink

def Function.Injective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : Semigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : Semigroup M₁

A type endowed with * is a semigroup, if it admits an injective map that preserves * to a semigroup. See note [reducible non-instances].

Equations

• Function.Injective.semigroup f hf mul = let src := inst; Semigroup.mk (_ : ∀ (x y z : M₁), x * y * z = x * (y * z))

ink

def Function.Injective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommSemigroup M₁

A type endowed with + is an additive commutative semigroup,if it admits an injective map that preserves + to an additive commutative semigroup.

Equations

• Function.Injective.addCommSemigroup f hf mul = let src := Function.Injective.addSemigroup f hf mul; AddCommSemigroup.mk (_ : ∀ (x y : M₁), x + y = y + x)

ink

def Function.Injective.addCommSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddCommSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) : x + y = y + x

Equations

• (_ : x + y = y + x) = hf (x + y) (y + x) (_ : f (x + y) = f (y + x))

ink

def Function.Injective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : CommSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommSemigroup M₁

A type endowed with * is a commutative semigroup, if it admits an injective map that preserves * to a commutative semigroup. See note [reducible non-instances].

Equations

• Function.Injective.commSemigroup f hf mul = let src := Function.Injective.semigroup f hf mul; CommSemigroup.mk (_ : ∀ (x y : M₁), x * y = y * x)

ink

def Function.Injective.addLeftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddLeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddLeftCancelSemigroup M₁

A type endowed with + is an additive left cancel semigroup, if it admits an injective map that preserves + to an additive left cancel semigroup.

Equations

• Function.Injective.addLeftCancelSemigroup f hf mul = let src := Function.Injective.addSemigroup f hf mul; AddLeftCancelSemigroup.mk (_ : ∀ (x y z : M₁), x + y = x + z → y = z)

ink

def Function.Injective.addLeftCancelSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddLeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) (H : x + y = x + z) : y = z

Equations

• (_ : y = z) = hf y z (_ : f y = f z)

ink

def Function.Injective.leftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : LeftCancelSemigroup M₁

A type endowed with * is a left cancel semigroup, if it admits an injective map that preserves * to a left cancel semigroup. See note [reducible non-instances].

Equations

• Function.Injective.leftCancelSemigroup f hf mul = let src := Function.Injective.semigroup f hf mul; LeftCancelSemigroup.mk (_ : ∀ (x y z : M₁), x * y = x * z → y = z)

ink

def Function.Injective.addRightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddRightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddRightCancelSemigroup M₁

A type endowed with + is an additive right cancel semigroup, if it admits an injective map that preserves + to an additive right cancel semigroup.

Equations

• Function.Injective.addRightCancelSemigroup f hf mul = let src := Function.Injective.addSemigroup f hf mul; AddRightCancelSemigroup.mk (_ : ∀ (x y z : M₁), x + y = z + y → x = z)

ink

def Function.Injective.addRightCancelSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : AddRightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) (H : x + y = z + y) : x = z

Equations

• (_ : x = z) = hf x z (_ : f x = f z)

ink

def Function.Injective.rightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : RightCancelSemigroup M₁

A type endowed with * is a right cancel semigroup, if it admits an injective map that preserves * to a right cancel semigroup. See note [reducible non-instances].

Equations

• Function.Injective.rightCancelSemigroup f hf mul = let src := Function.Injective.semigroup f hf mul; RightCancelSemigroup.mk (_ : ∀ (x y z : M₁), x * y = z * y → x = z)

ink

def Function.Injective.addZeroClass.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : AddZeroClass M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) : x + 0 = x

Equations

• (_ : x + 0 = x) = hf (x + 0) x (_ : f (x + 0) = f x)

ink

def Function.Injective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : AddZeroClass M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddZeroClass M₁

A type endowed with 0 and + is an AddZeroClass, if it admits an injective map that preserves 0 and + to an AddZeroClass.

Equations

• Function.Injective.addZeroClass f hf one mul = let src := inst; let src_1 := inst; AddZeroClass.mk (_ : ∀ (x : M₁), 0 + x = x) (_ : ∀ (x : M₁), x + 0 = x)

ink

def Function.Injective.addZeroClass.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : AddZeroClass M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) : 0 + x = x

Equations

• (_ : 0 + x = x) = hf (0 + x) x (_ : f (0 + x) = f x)

ink

def Function.Injective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : MulOneClass M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : MulOneClass M₁

A type endowed with 1 and * is a MulOneClass, if it admits an injective map that preserves 1 and * to a MulOneClass. See note [reducible non-instances].

Equations

• Function.Injective.mulOneClass f hf one mul = let src := inst; let src_1 := inst; MulOneClass.mk (_ : ∀ (x : M₁), 1 * x = x) (_ : ∀ (x : M₁), x * 1 = x)

ink

def Function.Injective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddMonoid M₁

A type endowed with 0 and + is an additive monoid, if it admits an injective map that preserves 0 and + to an additive monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (x : M₁) : (fun n x => n • x) 0 x = 0

Equations

• (_ : (fun n x => n • x) 0 x = 0) = hf ((fun n x => n • x) 0 x) 0 (_ : f ((fun n x => n • x) 0 x) = f 0)

ink

def Function.Injective.addMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (n : ℕ) (x : M₁) : (fun n x => n • x) (n + 1) x = x + (fun n x => n • x) n x

Equations

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

ink

def Function.Injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Monoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₁

A type endowed with 1 and * is a monoid, if it admits an injective map that preserves 1 and * to a monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addMonoidWithOne {M₂ : Type u_1} {M₁ : Type u_2} [inst : Zero M₁] [inst : One M₁] [inst : Add M₁] [inst : SMul ℕ M₁] [inst : NatCast M₁] [inst : AddMonoidWithOne M₂] (f : M₁ → M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : AddMonoidWithOne M₁

A type endowed with 0, 1 and + is an additive monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive monoid with one. See note [reducible non-instances].

Equations

• Function.Injective.addMonoidWithOne f hf zero one add nsmul nat_cast = let src := Function.Injective.addMonoid f hf zero add nsmul; AddMonoidWithOne.mk

ink

def Function.Injective.addLeftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddLeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddLeftCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid, if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

Equations

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

ink

def Function.Injective.leftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : LeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : LeftCancelMonoid M₁

A type endowed with 1 and * is a left cancel monoid, if it admits an injective map that preserves 1 and * to a left cancel monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addRightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddRightCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddRightCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

Equations

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

ink

def Function.Injective.rightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : RightCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : RightCancelMonoid M₁

A type endowed with 1 and * is a right cancel monoid, if it admits an injective map that preserves 1 and * to a right cancel monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCancelMonoid M₁

A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

Equations

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

ink

def Function.Injective.addCancelMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (a : M₁) (b : M₁) (c : M₁) : a + b = c + b → a = c

Equations

• (_ : ∀ (a b c : M₁), a + b = c + b → a = c) = (_ : ∀ (a b c : M₁), a + b = c + b → a = c)

ink

def Function.Injective.cancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : CancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoid M₁

A type endowed with 1 and * is a cancel monoid, if it admits an injective map that preserves 1 and * to a cancel monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCommMonoid M₁

A type endowed with 0 and + is an additive commutative monoid, if it admits an injective map that preserves 0 and + to an additive commutative monoid.

Equations

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

ink

def Function.Injective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : CommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₁

A type endowed with 1 and * is a commutative monoid, if it admits an injective map that preserves 1 and * to a commutative monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCommMonoidWithOne {M₂ : Type u_1} {M₁ : Type u_2} [inst : Zero M₁] [inst : One M₁] [inst : Add M₁] [inst : SMul ℕ M₁] [inst : NatCast M₁] [inst : AddCommMonoidWithOne M₂] (f : M₁ → M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : AddCommMonoidWithOne M₁

A type endowed with 0, 1 and + is an additive commutative monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative monoid with one. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCancelCommMonoid M₁

A type endowed with 0 and + is an additive cancel commutative monoid, if it admits an injective map that preserves 0 and + to an additive cancel commutative monoid.

Equations

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

ink

def Function.Injective.addCancelCommMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (a : M₁) : 0 + a = a

Equations

• (_ : ∀ (a : M₁), 0 + a = a) = (_ : ∀ (a : M₁), 0 + a = a)

ink

def Function.Injective.addCancelCommMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (a : M₁) : a + 0 = a

Equations

• (_ : ∀ (a : M₁), a + 0 = a) = (_ : ∀ (a : M₁), a + 0 = a)

ink

def Function.Injective.addCancelCommMonoid.proof_4 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (n : ℕ) (x : M₁) : AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Equations

• (_ : ∀ (n : ℕ) (x : M₁), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x) = (_ : ∀ (n : ℕ) (x : M₁), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x)

ink

def Function.Injective.addCancelCommMonoid.proof_3 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (x : M₁) : AddMonoid.nsmul 0 x = 0

Equations

• (_ : ∀ (x : M₁), AddMonoid.nsmul 0 x = 0) = (_ : ∀ (x : M₁), AddMonoid.nsmul 0 x = 0)

ink

def Function.Injective.cancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : CancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoid M₁

A type endowed with 1 and * is a cancel commutative monoid, if it admits an injective map that preserves 1 and * to a cancel commutative monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.involutiveNeg.proof_1 {M₂ : Type u_2} {M₁ : Type u_1} [inst : Neg M₁] [inst : InvolutiveNeg M₂] (f : M₁ → M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) (x : M₁) : - -x = x

Equations

• (_ : - -x = x) = hf (- -x) x (_ : f (- -x) = f x)

ink

def Function.Injective.involutiveNeg {M₂ : Type u_1} {M₁ : Type u_2} [inst : Neg M₁] [inst : InvolutiveNeg M₂] (f : M₁ → M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) : InvolutiveNeg M₁

A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

Equations

• Function.Injective.involutiveNeg f hf inv = InvolutiveNeg.mk (_ : ∀ (x : M₁), - -x = x)

ink

def Function.Injective.involutiveInv {M₂ : Type u_1} {M₁ : Type u_2} [inst : Inv M₁] [inst : InvolutiveInv M₂] (f : M₁ → M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁

A type has an involutive inversion if it admits a surjective map that preserves ⁻¹⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

Equations

• Function.Injective.involutiveInv f hf inv = InvolutiveInv.mk (_ : ∀ (x : M₁), x⁻¹⁻¹ = x)

ink

def Function.Injective.subNegMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : SMul ℤ M₁] [inst : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (x : M₁) : (fun n x => n • x) 0 x = 0

Equations

• (_ : (fun n x => n • x) 0 x = 0) = hf ((fun n x => n • x) 0 x) 0 (_ : f ((fun n x => n • x) 0 x) = f 0)

ink

def Function.Injective.subNegMonoid.proof_3 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : SMul ℤ M₁] [inst : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (n : ℕ) (x : M₁) : (fun n x => n • x) (Int.ofNat (Nat.succ n)) x = x + (fun n x => n • x) (Int.ofNat n) x

Equations

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

ink

def Function.Injective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubNegMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubNegMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

Equations

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

ink

def Function.Injective.subNegMonoid.proof_4 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Neg M₁] [inst : SMul ℤ M₁] [inst : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (n : ℕ) (x : M₁) : (fun n x => n • x) (Int.negSucc n) x = -(fun n x => n • x) (↑(Nat.succ n)) x

Equations

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

ink

def Function.Injective.subNegMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SubNegMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (x : M₁) (y : M₁) : x - y = x + -y

Equations

• (_ : x - y = x + -y) = hf (x - y) (x + -y) (_ : f (x - y) = f (x + -y))

ink

def Function.Injective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Inv M₁] [inst : Div M₁] [inst : Pow M₁ ℤ] [inst : DivInvMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₁

A type endowed with 1, *, ⁻¹⁻¹, and / is a DivInvMonoid if it admits an injective map that preserves 1, *, ⁻¹⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.subtractionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : SubtractionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubtractionMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubtractionMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

Equations

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

ink

def Function.Injective.subtractionMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : SubtractionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (x : M₁) (y : M₁) : -(x + y) = -y + -x

Equations

• (_ : -(x + y) = -y + -x) = hf (-(x + y)) (-y + -x) (_ : f (-(x + y)) = f (-y + -x))

ink

def Function.Injective.subtractionMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : SubtractionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (x : M₁) (y : M₁) (h : x + y = 0) : -x = y

Equations

• (_ : -x = y) = hf (-x) y (_ : f (-x) = f y)

ink

def Function.Injective.divisionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Inv M₁] [inst : Div M₁] [inst : Pow M₁ ℤ] [inst : DivisionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionMonoid M₁

A type endowed with 1, *, ⁻¹⁻¹, and / is a DivisionMonoid if it admits an injective map that preserves 1, *, ⁻¹⁻¹, and / to a DivisionMonoid. See note [reducible non-instances]

Equations

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

ink

def Function.Injective.subtractionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : SubtractionCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubtractionCommMonoid M₁

A type endowed with 0, +, unary -, and binary - is a SubtractionCommMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionCommMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

Equations

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

ink

def Function.Injective.divisionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Inv M₁] [inst : Div M₁] [inst : Pow M₁ ℤ] [inst : DivisionCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivisionCommMonoid M₁

A type endowed with 1, *, ⁻¹⁻¹, and / is a DivisionCommMonoid if it admits an injective map that preserves 1, *, ⁻¹⁻¹, and / to a DivisionCommMonoid. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : AddGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddGroup M₁

A type endowed with 0 and + is an additive group, if it admits an injective map that preserves 0 and + to an additive group.

Equations

• Function.Injective.addGroup f hf one mul inv div npow zpow = let src := Function.Injective.subNegMonoid f hf one mul inv div npow zpow; AddGroup.mk (_ : ∀ (x : M₁), -x + x = 0)

ink

def Function.Injective.addGroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : AddGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (x : M₁) : -x + x = 0

Equations

• (_ : -x + x = 0) = hf (-x + x) 0 (_ : f (-x + x) = f 0)

ink

def Function.Injective.group {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Inv M₁] [inst : Div M₁] [inst : Pow M₁ ℤ] [inst : Group M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₁

A type endowed with 1, * and ⁻¹⁻¹ is a group, if it admits an injective map that preserves 1, * and ⁻¹⁻¹ to a group. See note [reducible non-instances].

Equations

• Function.Injective.group f hf one mul inv div npow zpow = let src := Function.Injective.divInvMonoid f hf one mul inv div npow zpow; Group.mk (_ : ∀ (x : M₁), x⁻¹ * x = 1)

ink

def Function.Injective.addGroupWithOne {M₂ : Type u_1} {M₁ : Type u_2} [inst : Zero M₁] [inst : One M₁] [inst : Add M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : NatCast M₁] [inst : IntCast M₁] [inst : AddGroupWithOne M₂] (f : M₁ → M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : AddGroupWithOne M₁

A type endowed with 0, 1 and + is an additive group with one, if it admits an injective map that preserves 0, 1 and + to an additive group with one. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst : Zero M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : AddCommGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddCommGroup M₁

A type endowed with 0 and + is an additive commutative group, if it admits an injective map that preserves 0 and + to an additive commutative group.

Equations

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

ink

def Function.Injective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst : One M₁] [inst : Pow M₁ ℕ] [inst : Inv M₁] [inst : Div M₁] [inst : Pow M₁ ℤ] [inst : CommGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₁

A type endowed with 1, * and ⁻¹⁻¹ is a commutative group, if it admits an injective map that preserves 1, * and ⁻¹⁻¹ to a commutative group. See note [reducible non-instances].

Equations

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

ink

def Function.Injective.addCommGroupWithOne {M₂ : Type u_1} {M₁ : Type u_2} [inst : Zero M₁] [inst : One M₁] [inst : Add M₁] [inst : SMul ℕ M₁] [inst : Neg M₁] [inst : Sub M₁] [inst : SMul ℤ M₁] [inst : NatCast M₁] [inst : IntCast M₁] [inst : AddCommGroupWithOne M₂] (f : M₁ → M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : AddCommGroupWithOne M₁

A type endowed with 0, 1 and + is an additive commutative group with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative group with one. See note [reducible non-instances].

Equations

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

Surjective

ink

def Function.Surjective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : AddSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddSemigroup M₂

A type endowed with + is an additive semigroup, if it admits a surjective map that preserves + from an additive semigroup.

Equations

• Function.Surjective.addSemigroup f hf mul = let src := inst; AddSemigroup.mk (_ : ∀ (y₁ y₂ y₃ : M₂), y₁ + y₂ + y₃ = y₁ + (y₂ + y₃))

ink

def Function.Surjective.addSemigroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : AddSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y₁ : M₂) (y₂ : M₂) (y₃ : M₂) : y₁ + y₂ + y₃ = y₁ + (y₂ + y₃)

Equations

• (_ : ∀ (y₁ y₂ y₃ : M₂), y₁ + y₂ + y₃ = y₁ + (y₂ + y₃)) = (_ : ∀ (y₁ y₂ y₃ : M₂), y₁ + y₂ + y₃ = y₁ + (y₂ + y₃))

ink

def Function.Surjective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : Semigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : Semigroup M₂

A type endowed with * is a semigroup, if it admits a surjective map that preserves * from a semigroup. See note [reducible non-instances].

Equations

• Function.Surjective.semigroup f hf mul = let src := inst; Semigroup.mk (_ : ∀ (y₁ y₂ y₃ : M₂), y₁ * y₂ * y₃ = y₁ * (y₂ * y₃))

ink

def Function.Surjective.addCommSemigroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : AddCommSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y₁ : M₂) (y₂ : M₂) : y₁ + y₂ = y₂ + y₁

Equations

• (_ : ∀ (y₁ y₂ : M₂), y₁ + y₂ = y₂ + y₁) = (_ : ∀ (y₁ y₂ : M₂), y₁ + y₂ = y₂ + y₁)

ink

def Function.Surjective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : AddCommSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddCommSemigroup M₂

A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

Equations

• Function.Surjective.addCommSemigroup f hf mul = let src := Function.Surjective.addSemigroup f hf mul; AddCommSemigroup.mk (_ : ∀ (y₁ y₂ : M₂), y₁ + y₂ = y₂ + y₁)

ink

def Function.Surjective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : CommSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : CommSemigroup M₂

A type endowed with * is a commutative semigroup, if it admits a surjective map that preserves * from a commutative semigroup. See note [reducible non-instances].

Equations

• Function.Surjective.commSemigroup f hf mul = let src := Function.Surjective.semigroup f hf mul; CommSemigroup.mk (_ : ∀ (y₁ y₂ : M₂), y₁ * y₂ = y₂ * y₁)

ink

def Function.Surjective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : AddZeroClass M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) : AddZeroClass M₂

A type endowed with 0 and + is an AddZeroClass, if it admits a surjective map that preserves 0 and + to an AddZeroClass.

Equations

• Function.Surjective.addZeroClass f hf one mul = let src := inst; let src_1 := inst; AddZeroClass.mk (_ : ∀ (y : M₂), 0 + y = y) (_ : ∀ (y : M₂), y + 0 = y)

ink

def Function.Surjective.addZeroClass.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : AddZeroClass M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y : M₂) : 0 + y = y

Equations

• (_ : ∀ (y : M₂), 0 + y = y) = (_ : ∀ (y : M₂), 0 + y = y)

ink

def Function.Surjective.addZeroClass.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : AddZeroClass M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y : M₂) : y + 0 = y

Equations

• (_ : ∀ (y : M₂), y + 0 = y) = (_ : ∀ (y : M₂), y + 0 = y)

ink

def Function.Surjective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : MulOneClass M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) : MulOneClass M₂

A type endowed with 1 and * is a MulOneClass, if it admits a surjective map that preserves 1 and * from a MulOneClass. See note [reducible non-instances].

Equations

• Function.Surjective.mulOneClass f hf one mul = let src := inst; let src_1 := inst; MulOneClass.mk (_ : ∀ (y : M₂), 1 * y = y) (_ : ∀ (y : M₂), y * 1 = y)

ink

def Function.Surjective.addMonoid.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : AddMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (y : M₂) : (fun n x => n • x) 0 y = 0

Equations

• (_ : ∀ (y : M₂), (fun n x => n • x) 0 y = 0) = (_ : ∀ (y : M₂), (fun n x => n • x) 0 y = 0)

ink

def Function.Surjective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : AddMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddMonoid M₂

A type endowed with 0 and + is an additive monoid, if it admits a surjective map that preserves 0 and + to an additive monoid. This version takes a custom nsmul as a [SMul ℕ M₂] argument.

Equations

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

ink

def Function.Surjective.addMonoid.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : SMul ℕ M₂] [inst : AddMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (n : ℕ) (y : M₂) : (fun n x => n • x) (n + 1) y = y + (fun n x => n • x) n y

Equations

• (_ : ∀ (y : M₂), (fun n x => n • x) (n + 1) y = y + (fun n x => n • x) n y) = (_ : ∀ (y : M₂), (fun n x => n • x) (n + 1) y = y + (fun n x => n • x) n y)

ink

def Function.Surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : Pow M₂ ℕ] [inst : Monoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : Monoid M₂

A type endowed with 1 and * is a monoid, if it admits a surjective map that preserves 1 and * to a monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.addMonoidWithOne {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₂] [inst : One M₂] [inst : Add M₂] [inst : SMul ℕ M₂] [inst : NatCast M₂] [inst : AddMonoidWithOne M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : AddMonoidWithOne M₂

A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

Equations

• Function.Surjective.addMonoidWithOne f hf zero one add nsmul nat_cast = let src := Function.Surjective.addMonoid f hf zero add nsmul; AddMonoidWithOne.mk

ink

def Function.Surjective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : AddCommMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) : AddCommMonoid M₂

A type endowed with 0 and + is an additive commutative monoid, if it admits a surjective map that preserves 0 and + to an additive commutative monoid.

Equations

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

ink

def Function.Surjective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : Pow M₂ ℕ] [inst : CommMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoid M₂

A type endowed with 1 and * is a commutative monoid, if it admits a surjective map that preserves 1 and * from a commutative monoid. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.addCommMonoidWithOne {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₂] [inst : One M₂] [inst : Add M₂] [inst : SMul ℕ M₂] [inst : NatCast M₂] [inst : AddCommMonoidWithOne M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) : AddCommMonoidWithOne M₂

A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.involutiveNeg.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Neg M₂] [inst : InvolutiveNeg M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) (y : M₂) : - -y = y

Equations

• (_ : ∀ (y : M₂), - -y = y) = (_ : ∀ (y : M₂), - -y = y)

ink

def Function.Surjective.involutiveNeg {M₁ : Type u_1} {M₂ : Type u_2} [inst : Neg M₂] [inst : InvolutiveNeg M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) : InvolutiveNeg M₂

A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

Equations

• Function.Surjective.involutiveNeg f hf inv = InvolutiveNeg.mk (_ : ∀ (y : M₂), - -y = y)

ink

def Function.Surjective.involutiveInv {M₁ : Type u_1} {M₂ : Type u_2} [inst : Inv M₂] [inst : InvolutiveInv M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₂

A type has an involutive inversion if it admits a surjective map that preserves ⁻¹⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

Equations

• Function.Surjective.involutiveInv f hf inv = InvolutiveInv.mk (_ : ∀ (y : M₂), y⁻¹⁻¹ = y)

ink

def Function.Surjective.subNegMonoid.proof_4 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Neg M₂] [inst : SMul ℤ M₂] [inst : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (n : ℕ) (y : M₂) : (fun n x => n • x) (Int.negSucc n) y = -(fun n x => n • x) (↑(Nat.succ n)) y

Equations

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

ink

def Function.Surjective.subNegMonoid.proof_3 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : SMul ℤ M₂] [inst : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (n : ℕ) (y : M₂) : (fun n x => n • x) (Int.ofNat (Nat.succ n)) y = y + (fun n x => n • x) (Int.ofNat n) y

Equations

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

ink

def Function.Surjective.subNegMonoid.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : SMul ℤ M₂] [inst : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (y : M₂) : (fun n x => n • x) 0 y = 0

Equations

• (_ : ∀ (y : M₂), (fun n x => n • x) 0 y = 0) = (_ : ∀ (y : M₂), (fun n x => n • x) 0 y = 0)

ink

def Function.Surjective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℤ M₂] [inst : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : SubNegMonoid M₂

A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits a surjective map that preserves 0, +, unary -, and binary - to a SubNegMonoid.

Equations

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

ink

def Function.Surjective.subNegMonoid.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (y₁ : M₂) (y₂ : M₂) : y₁ - y₂ = y₁ + -y₂

Equations

• (_ : ∀ (y₁ y₂ : M₂), y₁ - y₂ = y₁ + -y₂) = (_ : ∀ (y₁ y₂ : M₂), y₁ - y₂ = y₁ + -y₂)

ink

def Function.Surjective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : Pow M₂ ℕ] [inst : Inv M₂] [inst : Div M₂] [inst : Pow M₂ ℤ] [inst : DivInvMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : DivInvMonoid M₂

A type endowed with 1, *, ⁻¹⁻¹, and / is a DivInvMonoid if it admits a surjective map that preserves 1, *, ⁻¹⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.addGroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℤ M₂] [inst : AddGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (y : M₂) : -y + y = 0

Equations

• (_ : ∀ (y : M₂), -y + y = 0) = (_ : ∀ (y : M₂), -y + y = 0)

ink

def Function.Surjective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℤ M₂] [inst : AddGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddGroup M₂

A type endowed with 0 and + is an additive group, if it admits a surjective map that preserves 0 and + to an additive group.

Equations

• Function.Surjective.addGroup f hf one mul inv div npow zpow = let src := Function.Surjective.subNegMonoid f hf one mul inv div npow zpow; AddGroup.mk (_ : ∀ (y : M₂), -y + y = 0)

ink

def Function.Surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : Pow M₂ ℕ] [inst : Inv M₂] [inst : Div M₂] [inst : Pow M₂ ℤ] [inst : Group M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : Group M₂

A type endowed with 1, * and ⁻¹⁻¹ is a group, if it admits a surjective map that preserves 1, * and ⁻¹⁻¹ to a group. See note [reducible non-instances].

Equations

• Function.Surjective.group f hf one mul inv div npow zpow = let src := Function.Surjective.divInvMonoid f hf one mul inv div npow zpow; Group.mk (_ : ∀ (y : M₂), y⁻¹ * y = 1)

ink

def Function.Surjective.addGroupWithOne {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₂] [inst : One M₂] [inst : Add M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℕ M₂] [inst : SMul ℤ M₂] [inst : NatCast M₂] [inst : IntCast M₂] [inst : AddGroupWithOne M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : AddGroupWithOne M₂

A type endowed with 0, 1, + is an additive group with one, if it admits a surjective map that preserves 0, 1, and + to an additive group with one. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst : Zero M₂] [inst : SMul ℕ M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℤ M₂] [inst : AddCommGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) : AddCommGroup M₂

A type endowed with 0 and + is an additive commutative group, if it admits a surjective map that preserves 0 and + to an additive commutative group.

Equations

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

ink

def Function.Surjective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst : One M₂] [inst : Pow M₂ ℕ] [inst : Inv M₂] [inst : Div M₂] [inst : Pow M₂ ℤ] [inst : CommGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroup M₂

A type endowed with 1, *, ⁻¹⁻¹, and / is a commutative group, if it admits a surjective map that preserves 1, *, ⁻¹⁻¹, and / from a commutative group. See note [reducible non-instances].

Equations

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

ink

def Function.Surjective.addCommGroupWithOne {M₁ : Type u_1} {M₂ : Type u_2} [inst : Zero M₂] [inst : One M₂] [inst : Add M₂] [inst : Neg M₂] [inst : Sub M₂] [inst : SMul ℕ M₂] [inst : SMul ℤ M₂] [inst : NatCast M₂] [inst : IntCast M₂] [inst : AddCommGroupWithOne M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) (nat_cast : ∀ (n : ℕ), f ↑n = ↑n) (int_cast : ∀ (n : ℤ), f ↑n = ↑n) : AddCommGroupWithOne M₂

A type endowed with 0, 1, + is an additive commutative group with one, if it admits a surjective map that preserves 0, 1, and + to an additive commutative group with one. See note [reducible non-instances].

Equations

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