# Documentation

Mathlib.Algebra.Group.Hom.Defs

# Monoid and group homomorphisms #

This file defines the bundled structures for monoid and group homomorphisms. Namely, we define MonoidHom (resp., AddMonoidHom) to be bundled homomorphisms between multiplicative (resp., additive) monoids or groups.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

This file also defines the lesser-used (and notation-less) homomorphism types which are used as building blocks for other homomorphisms:

• ZeroHom
• OneHom
• AddHom
• MulHom
• MonoidWithZeroHom

## Notations #

• →+: Bundled AddMonoid homs. Also use for AddGroup homs.
• →*: Bundled Monoid homs. Also use for Group homs.
• →*₀: Bundled MonoidWithZero homs. Also use for GroupWithZero homs.
• →ₙ*: Bundled Semigroup homs.

## Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no GroupHom -- the idea is that MonoidHom is used. The constructor for MonoidHom needs a proof of map_one as well as map_mul; a separate constructor MonoidHom.mk' will construct group homs (i.e. monoid homs between groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type MonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Historically this file also included definitions of unbundled homomorphism classes; they were deprecated and moved to Deprecated/Group.

## Tags #

structure ZeroHom (M : Type u_9) (N : Type u_10) [Zero M] [Zero N] :
Type (max u_10 u_9)

ZeroHom M N is the type of functions M → N that preserve zero.

When possible, instead of parametrizing results over (f : ZeroHom M N), you should parametrize over (F : Type*) [ZeroHomClass F M N] (f : F).

When you extend this structure, make sure to also extend ZeroHomClass.

• toFun : MN

The underlying function

• map_zero' : = 0

The proposition that the function preserves 0

Instances For
class ZeroHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [Zero M] [Zero N] extends :
Type (max (max u_10 u_11) u_9)

ZeroHomClass F M N states that F is a type of zero-preserving homomorphisms.

You should extend this typeclass when you extend ZeroHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

Instances
structure AddHom (M : Type u_9) (N : Type u_10) [Add M] [Add N] :
Type (max u_10 u_9)

AddHom M N is the type of functions M → N that preserve addition.

When possible, instead of parametrizing results over (f : AddHom M N), you should parametrize over (F : Type*) [AddHomClass F M N] (f : F).

When you extend this structure, make sure to extend AddHomClass.

• toFun : MN

The underlying function

• map_add' : ∀ (x y : M), AddHom.toFun s (x + y) = +

The proposition that the function preserves addition

Instances For
class AddHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [Add M] [Add N] extends :
Type (max (max u_10 u_11) u_9)

AddHomClass F M N states that F is a type of addition-preserving homomorphisms. You should declare an instance of this typeclass when you extend AddHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

The proposition that the function preserves addition

Instances
structure AddMonoidHom (M : Type u_9) (N : Type u_10) [] [] extends :
Type (max u_10 u_9)

M →+ N is the type of functions M → N that preserve the AddZeroClass structure.

AddMonoidHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [AddMonoidHomClass F M N] (f : F).

When you extend this structure, make sure to extend AddMonoidHomClass.

Instances For

M →+ N denotes the type of additive monoid homomorphisms from M to N.

Equations
Instances For
class AddMonoidHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [] [] extends :
Type (max (max u_10 u_11) u_9)

AddMonoidHomClass F M N states that F is a type of AddZeroClass-preserving homomorphisms.

You should also extend this typeclass when you extend AddMonoidHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

Instances
structure OneHom (M : Type u_9) (N : Type u_10) [One M] [One N] :
Type (max u_10 u_9)

OneHom M N is the type of functions M → N that preserve one.

When possible, instead of parametrizing results over (f : OneHom M N), you should parametrize over (F : Type*) [OneHomClass F M N] (f : F).

When you extend this structure, make sure to also extend OneHomClass.

• toFun : MN

The underlying function

• map_one' : = 1

The proposition that the function preserves 1

Instances For
class OneHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [One M] [One N] extends :
Type (max (max u_10 u_11) u_9)

OneHomClass F M N states that F is a type of one-preserving homomorphisms. You should extend this typeclass when you extend OneHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_one : ∀ (f : F), f 1 = 1

The proposition that the function preserves 1

Instances
theorem ZeroHom.zeroHomClass.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) (g : ZeroHom M N) (h : f.toFun = g.toFun) :
f = g
instance ZeroHom.zeroHomClass {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
Equations
instance OneHom.oneHomClass {M : Type u_3} {N : Type u_4} [One M] [One N] :
Equations
@[simp]
theorem map_zero {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [ZeroHomClass F M N] (f : F) :
f 0 = 0
@[simp]
theorem map_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [OneHomClass F M N] (f : F) :
f 1 = 1
theorem Subsingleton.of_zeroHomClass {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [] [ZeroHomClass F M N] :
theorem Subsingleton.of_oneHomClass {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [] [OneHomClass F M N] :

In principle this could be an instance, but in practice it causes performance issues.

instance instSubsingletonZeroHom {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] [] :
Equations
instance instSubsingletonOneHom {M : Type u_3} {N : Type u_4} [One M] [One N] [] :
Equations
theorem map_eq_zero_iff {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [ZeroHomClass F M N] (f : F) (hf : ) {x : M} :
f x = 0 x = 0
theorem map_eq_one_iff {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [OneHomClass F M N] (f : F) (hf : ) {x : M} :
f x = 1 x = 1
theorem map_ne_zero_iff {R : Type u_9} {S : Type u_10} {F : Type u_11} [Zero R] [Zero S] [ZeroHomClass F R S] (f : F) (hf : ) {x : R} :
f x 0 x 0
theorem map_ne_one_iff {R : Type u_9} {S : Type u_10} {F : Type u_11} [One R] [One S] [OneHomClass F R S] (f : F) (hf : ) {x : R} :
f x 1 x 1
theorem ne_zero_of_map {R : Type u_9} {S : Type u_10} {F : Type u_11} [Zero R] [Zero S] [ZeroHomClass F R S] {f : F} {x : R} (hx : f x 0) :
x 0
theorem ne_one_of_map {R : Type u_9} {S : Type u_10} {F : Type u_11} [One R] [One S] [OneHomClass F R S] {f : F} {x : R} (hx : f x 1) :
x 1
def ZeroHomClass.toZeroHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [ZeroHomClass F M N] (f : F) :

Turn an element of a type F satisfying ZeroHomClass F M N into an actual ZeroHom. This is declared as the default coercion from F to ZeroHom M N.

Equations
• f = { toFun := f, map_zero' := (_ : f 0 = 0) }
Instances For
def OneHomClass.toOneHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [OneHomClass F M N] (f : F) :
OneHom M N

Turn an element of a type F satisfying OneHomClass F M N into an actual OneHom. This is declared as the default coercion from F to OneHom M N.

Equations
• f = { toFun := f, map_one' := (_ : f 1 = 1) }
Instances For
instance instCoeTCZeroHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [ZeroHomClass F M N] :
CoeTC F (ZeroHom M N)

Any type satisfying ZeroHomClass can be cast into ZeroHom via ZeroHomClass.toZeroHom.

Equations
• instCoeTCZeroHom = { coe := ZeroHomClass.toZeroHom }
instance instCoeTCOneHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [OneHomClass F M N] :
CoeTC F (OneHom M N)

Any type satisfying OneHomClass can be cast into OneHom via OneHomClass.toOneHom.

Equations
• instCoeTCOneHom = { coe := OneHomClass.toOneHom }
@[simp]
theorem ZeroHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [Zero M] [Zero N] [ZeroHomClass F M N] (f : F) :
f = f
@[simp]
theorem OneHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [One M] [One N] [OneHomClass F M N] (f : F) :
f = f
structure MulHom (M : Type u_9) (N : Type u_10) [Mul M] [Mul N] :
Type (max u_10 u_9)

M →ₙ* N is the type of functions M → N that preserve multiplication. The ₙ in the notation stands for "non-unital" because it is intended to match the notation for NonUnitalAlgHom and NonUnitalRingHom, so a MulHom is a non-unital monoid hom.

When possible, instead of parametrizing results over (f : M →ₙ* N), you should parametrize over (F : Type*) [MulHomClass F M N] (f : F). When you extend this structure, make sure to extend MulHomClass.

• toFun : MN

The underlying function

• map_mul' : ∀ (x y : M), MulHom.toFun s (x * y) = *

The proposition that the function preserves multiplication

Instances For

M →ₙ* N denotes the type of multiplication-preserving maps from M to N.

Equations
Instances For
class MulHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [Mul M] [Mul N] extends :
Type (max (max u_10 u_11) u_9)

MulHomClass F M N states that F is a type of multiplication-preserving homomorphisms.

You should declare an instance of this typeclass when you extend MulHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

The proposition that the function preserves multiplication

Instances
instance AddHom.addHomClass {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

AddHom is a type of addition-preserving homomorphisms

Equations
theorem AddHom.addHomClass.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (g : AddHom M N) (h : f.toFun = g.toFun) :
f = g
instance MulHom.mulHomClass {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

MulHom is a type of multiplication-preserving homomorphisms

Equations
@[simp]
theorem map_add {M : Type u_3} {N : Type u_4} {F : Type u_8} [Add M] [Add N] [AddHomClass F M N] (f : F) (x : M) (y : M) :
f (x + y) = f x + f y
@[simp]
theorem map_mul {M : Type u_3} {N : Type u_4} {F : Type u_8} [Mul M] [Mul N] [MulHomClass F M N] (f : F) (x : M) (y : M) :
f (x * y) = f x * f y
def AddHomClass.toAddHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Add M] [Add N] [AddHomClass F M N] (f : F) :

Turn an element of a type F satisfying AddHomClass F M N into an actual AddHom. This is declared as the default coercion from F to M →ₙ+ N.

Equations
• f = { toFun := f, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }
Instances For
def MulHomClass.toMulHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Mul M] [Mul N] [MulHomClass F M N] (f : F) :

Turn an element of a type F satisfying MulHomClass F M N into an actual MulHom. This is declared as the default coercion from F to M →ₙ* N.

Equations
• f = { toFun := f, map_mul' := (_ : ∀ (x y : M), f (x * y) = f x * f y) }
Instances For
instance instCoeTCAddHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Add M] [Add N] [AddHomClass F M N] :
CoeTC F (AddHom M N)

Any type satisfying AddHomClass can be cast into AddHom via AddHomClass.toAddHom.

Equations
instance instCoeTCMulHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [Mul M] [Mul N] [MulHomClass F M N] :
CoeTC F (M →ₙ* N)

Any type satisfying MulHomClass can be cast into MulHom via MulHomClass.toMulHom.

Equations
• instCoeTCMulHom = { coe := MulHomClass.toMulHom }
@[simp]
theorem AddHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [Add M] [Add N] [AddHomClass F M N] (f : F) :
f = f
@[simp]
theorem MulHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [Mul M] [Mul N] [MulHomClass F M N] (f : F) :
f = f
structure MonoidHom (M : Type u_9) (N : Type u_10) [] [] extends :
Type (max u_10 u_9)

M →* N is the type of functions M → N that preserve the Monoid structure. MonoidHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [MonoidHomClass F M N] (f : F).

When you extend this structure, make sure to extend MonoidHomClass.

Instances For

M →* N denotes the type of monoid homomorphisms from M to N.

Equations
Instances For
class MonoidHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [] [] extends :
Type (max (max u_10 u_11) u_9)

MonoidHomClass F M N states that F is a type of Monoid-preserving homomorphisms. You should also extend this typeclass when you extend MonoidHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1

The proposition that the function preserves 1

Instances
theorem AddMonoidHom.addMonoidHomClass.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M →+ N) (h : (fun (f : M →+ N) => f.toFun) f = (fun (f : M →+ N) => f.toFun) g) :
f = g
theorem AddMonoidHom.addMonoidHomClass.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) :
ZeroHom.toFun (f) 0 = 0
instance AddMonoidHom.addMonoidHomClass {M : Type u_3} {N : Type u_4} [] [] :
Equations
instance MonoidHom.monoidHomClass {M : Type u_3} {N : Type u_4} [] [] :
Equations
instance instSubsingletonAddMonoidHom {M : Type u_3} {N : Type u_4} [] [] [] :
Equations
instance instSubsingletonMonoidHom {M : Type u_3} {N : Type u_4} [] [] [] :
Equations
theorem AddMonoidHomClass.toAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} {F : Type u_3} [] [] [] (f : F) (x : M) (y : M) :
AddHom.toFun (f) (x + y) = AddHom.toFun (f) x + AddHom.toFun (f) y
theorem AddMonoidHomClass.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} {F : Type u_3} [] [] [] (f : F) :
ZeroHom.toFun (f) 0 = 0
def AddMonoidHomClass.toAddMonoidHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :
M →+ N

Turn an element of a type F satisfying AddMonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →+ N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MonoidHomClass.toMonoidHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :
M →* N

Turn an element of a type F satisfying MonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →* N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instCoeTCAddMonoidHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] :
CoeTC F (M →+ N)

Any type satisfying AddMonoidHomClass can be cast into AddMonoidHom via AddMonoidHomClass.toAddMonoidHom.

Equations
instance instCoeTCMonoidHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] :
CoeTC F (M →* N)

Any type satisfying MonoidHomClass can be cast into MonoidHom via MonoidHomClass.toMonoidHom.

Equations
• instCoeTCMonoidHom = { coe := MonoidHomClass.toMonoidHom }
@[simp]
theorem AddMonoidHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :
f = f
@[simp]
theorem MonoidHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :
f = f
theorem map_add_eq_zero {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {a : M} {b : M} (h : a + b = 0) :
f a + f b = 0
theorem map_mul_eq_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {a : M} {b : M} (h : a * b = 1) :
f a * f b = 1
theorem map_sub' {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (hf : ∀ (a : G), f (-a) = -f a) (a : G) (b : G) :
f (a - b) = f a - f b
theorem map_div' {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹) (a : G) (b : G) :
f (a / b) = f a / f b
@[simp]
theorem map_neg {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] (f : F) (a : G) :
f (-a) = -f a

Additive group homomorphisms preserve negation.

@[simp]
theorem map_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (a : G) :
f a⁻¹ = (f a)⁻¹

Group homomorphisms preserve inverse.

theorem map_add_neg {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] (f : F) (a : G) (b : G) :
f (a + -b) = f a + -f b

Additive group homomorphisms preserve subtraction.

theorem map_mul_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (a : G) (b : G) :
f (a * b⁻¹) = f a * (f b)⁻¹

Group homomorphisms preserve division.

@[simp]
theorem map_sub {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] (f : F) (a : G) (b : G) :
f (a - b) = f a - f b

Additive group homomorphisms preserve subtraction.

@[simp]
theorem map_div {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (a : G) (b : G) :
f (a / b) = f a / f b

Group homomorphisms preserve division.

abbrev map_nsmul.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(∀ (n : ), motive ())motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
@[simp]
theorem map_nsmul {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (n : ) (a : G) :
f (n a) = n f a
@[simp]
theorem map_pow {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (a : G) (n : ) :
f (a ^ n) = f a ^ n
abbrev map_zsmul'.match_1 (motive : ) :
∀ (x : ), (∀ (n : ), motive ())(∀ (n : ), motive ())motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem map_zsmul' {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (hf : ∀ (x : G), f (-x) = -f x) (a : G) (n : ) :
f (n a) = n f a
theorem map_zpow' {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹) (a : G) (n : ) :
f (a ^ n) = f a ^ n
@[simp]
theorem map_zsmul {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] (f : F) (n : ) (g : G) :
f (n g) = n f g

Additive group homomorphisms preserve integer scaling.

@[simp]
theorem map_zpow {G : Type u_6} {H : Type u_7} {F : Type u_8} [] [] [] (f : F) (g : G) (n : ) :
f (g ^ n) = f g ^ n

Group homomorphisms preserve integer power.

structure MonoidWithZeroHom (M : Type u_9) (N : Type u_10) [] [] extends :
Type (max u_10 u_9)

M →*₀ N is the type of functions M → N that preserve the MonoidWithZero structure.

MonoidWithZeroHom is also used for group homomorphisms.

When possible, instead of parametrizing results over (f : M →*₀ N), you should parametrize over (F : Type*) [MonoidWithZeroHomClass F M N] (f : F).

When you extend this structure, make sure to extend MonoidWithZeroHomClass.

Instances For

M →*₀ N denotes the type of zero-preserving monoid homomorphisms from M to N.

Equations
Instances For
class MonoidWithZeroHomClass (F : Type u_9) (M : outParam (Type u_10)) (N : outParam (Type u_11)) [] [] extends :
Type (max (max u_10 u_11) u_9)

MonoidWithZeroHomClass F M N states that F is a type of MonoidWithZero-preserving homomorphisms.

You should also extend this typeclass when you extend MonoidWithZeroHom.

• coe : FMN
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

Instances
Equations
instance instSubsingletonMonoidWithZeroHom {M : Type u_3} {N : Type u_4} [] [] [] :
Equations
def MonoidWithZeroHomClass.toMonoidWithZeroHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :

Turn an element of a type F satisfying MonoidWithZeroHomClass F M N into an actual MonoidWithZeroHom. This is declared as the default coercion from F to M →*₀ N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instCoeTCMonoidWithZeroHom {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] :
CoeTC F (M →*₀ N)

Any type satisfying MonoidWithZeroHomClass can be cast into MonoidWithZeroHom via MonoidWithZeroHomClass.toMonoidWithZeroHom.

Equations
• instCoeTCMonoidWithZeroHom = { coe := MonoidWithZeroHomClass.toMonoidWithZeroHom }
@[simp]
theorem MonoidWithZeroHom.coe_coe {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) :
f = f

Bundled morphisms can be down-cast to weaker bundlings

instance AddMonoidHom.coeToZeroHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →+ N) (ZeroHom M N)

AddMonoidHom down-cast to a ZeroHom, forgetting the additive property

Equations
• AddMonoidHom.coeToZeroHom = { coe := AddMonoidHom.toZeroHom }
instance MonoidHom.coeToOneHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →* N) (OneHom M N)

MonoidHom down-cast to a OneHom, forgetting the multiplicative property.

Equations
• MonoidHom.coeToOneHom = { coe := MonoidHom.toOneHom }
instance AddMonoidHom.coeToAddHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →+ N) (AddHom M N)

AddMonoidHom down-cast to an AddHom, forgetting the 0-preserving property.

Equations
instance MonoidHom.coeToMulHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →* N) (M →ₙ* N)

MonoidHom down-cast to a MulHom, forgetting the 1-preserving property.

Equations
• MonoidHom.coeToMulHom = { coe := MonoidHom.toMulHom }
instance MonoidWithZeroHom.coeToMonoidHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →*₀ N) (M →* N)

MonoidWithZeroHom down-cast to a MonoidHom, forgetting the 0-preserving property.

Equations
• MonoidWithZeroHom.coeToMonoidHom = { coe := MonoidWithZeroHom.toMonoidHom }
instance MonoidWithZeroHom.coeToZeroHom {M : Type u_3} {N : Type u_4} [] [] :
Coe (M →*₀ N) (ZeroHom M N)

MonoidWithZeroHom down-cast to a ZeroHom, forgetting the monoidal property.

Equations
• MonoidWithZeroHom.coeToZeroHom = { coe := MonoidWithZeroHom.toZeroHom }
@[simp]
theorem ZeroHom.coe_mk {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : MN) (h1 : f 0 = 0) :
{ toFun := f, map_zero' := h1 } = f
@[simp]
theorem OneHom.coe_mk {M : Type u_3} {N : Type u_4} [One M] [One N] (f : MN) (h1 : f 1 = 1) :
{ toFun := f, map_one' := h1 } = f
@[simp]
theorem ZeroHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) :
f.toFun = f
@[simp]
theorem OneHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) :
f.toFun = f
@[simp]
theorem AddHom.coe_mk {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : MN) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{ toFun := f, map_add' := hmul } = f
@[simp]
theorem MulHom.coe_mk {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : MN) (hmul : ∀ (x y : M), f (x * y) = f x * f y) :
{ toFun := f, map_mul' := hmul } = f
@[simp]
theorem AddHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) :
f.toFun = f
@[simp]
theorem MulHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) :
f.toFun = f
@[simp]
theorem AddMonoidHom.coe_mk {M : Type u_3} {N : Type u_4} [] [] (f : ZeroHom M N) (hmul : ∀ (x y : M), ZeroHom.toFun f (x + y) = + ) :
{ toZeroHom := f, map_add' := hmul } = f
@[simp]
theorem MonoidHom.coe_mk {M : Type u_3} {N : Type u_4} [] [] (f : OneHom M N) (hmul : ∀ (x y : M), OneHom.toFun f (x * y) = * ) :
{ toOneHom := f, map_mul' := hmul } = f
@[simp]
theorem AddMonoidHom.toZeroHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
f = f
@[simp]
theorem MonoidHom.toOneHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
f = f
@[simp]
theorem AddMonoidHom.toAddHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
(f).toFun = f
@[simp]
theorem MonoidHom.toMulHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
(f).toFun = f
theorem AddMonoidHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
f.toFun = f
theorem MonoidHom.toFun_eq_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
f.toFun = f
@[simp]
theorem MonoidWithZeroHom.coe_mk {M : Type u_3} {N : Type u_4} [] [] (f : ZeroHom M N) (h1 : = 1) (hmul : ∀ (x y : M), ZeroHom.toFun f (x * y) = * ) :
{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = f
@[simp]
theorem MonoidWithZeroHom.toZeroHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
f = f
theorem MonoidWithZeroHom.toMonoidHom_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
(f).toFun = f
theorem ZeroHom.ext {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] ⦃f : ZeroHom M N ⦃g : ZeroHom M N (h : ∀ (x : M), f x = g x) :
f = g
theorem OneHom.ext {M : Type u_3} {N : Type u_4} [One M] [One N] ⦃f : OneHom M N ⦃g : OneHom M N (h : ∀ (x : M), f x = g x) :
f = g
theorem AddHom.ext {M : Type u_3} {N : Type u_4} [Add M] [Add N] ⦃f : AddHom M N ⦃g : AddHom M N (h : ∀ (x : M), f x = g x) :
f = g
theorem MulHom.ext {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] ⦃f : M →ₙ* N ⦃g : M →ₙ* N (h : ∀ (x : M), f x = g x) :
f = g
theorem AddMonoidHom.ext {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →+ N ⦃g : M →+ N (h : ∀ (x : M), f x = g x) :
f = g
theorem MonoidHom.ext {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →* N ⦃g : M →* N (h : ∀ (x : M), f x = g x) :
f = g
theorem MonoidWithZeroHom.ext {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →*₀ N ⦃g : M →*₀ N (h : ∀ (x : M), f x = g x) :
f = g
theorem AddMonoidHom.mk'.proof_1 {M : Type u_2} {G : Type u_1} [] [] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
f 0 = 0
def AddMonoidHom.mk' {M : Type u_3} {G : Type u_6} [] [] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
M →+ G

Makes an additive group homomorphism from a proof that the map preserves addition.

Equations
• AddMonoidHom.mk' f map_mul = { toZeroHom := { toFun := f, map_zero' := (_ : f 0 = 0) }, map_add' := map_mul }
Instances For
@[simp]
theorem AddMonoidHom.mk'_apply {M : Type u_3} {G : Type u_6} [] [] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
(AddMonoidHom.mk' f map_mul) = f
@[simp]
theorem MonoidHom.mk'_apply {M : Type u_3} {G : Type u_6} [] [] (f : MG) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :
(MonoidHom.mk' f map_mul) = f
def MonoidHom.mk' {M : Type u_3} {G : Type u_6} [] [] (f : MG) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :
M →* G

Makes a group homomorphism from a proof that the map preserves multiplication.

Equations
• MonoidHom.mk' f map_mul = { toOneHom := { toFun := f, map_one' := (_ : f 1 = 1) }, map_mul' := map_mul }
Instances For
@[deprecated]
theorem ZeroHom.congr_fun {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {f : ZeroHom M N} {g : ZeroHom M N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem OneHom.congr_fun {M : Type u_3} {N : Type u_4} [One M] [One N] {f : OneHom M N} {g : OneHom M N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem AddHom.congr_fun {M : Type u_3} {N : Type u_4} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem MulHom.congr_fun {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem AddMonoidHom.congr_fun {M : Type u_3} {N : Type u_4} [] [] {f : M →+ N} {g : M →+ N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem MonoidHom.congr_fun {M : Type u_3} {N : Type u_4} [] [] {f : M →* N} {g : M →* N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem MonoidWithZeroHom.congr_fun {M : Type u_3} {N : Type u_4} [] [] {f : M →*₀ N} {g : M →*₀ N} (h : f = g) (x : M) :
f x = g x

Deprecated: use FunLike.congr_fun instead.

@[deprecated]
theorem ZeroHom.congr_arg {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem OneHom.congr_arg {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem AddHom.congr_arg {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem MulHom.congr_arg {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem AddMonoidHom.congr_arg {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem MonoidHom.congr_arg {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem MonoidWithZeroHom.congr_arg {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) {x : M} {y : M} (h : x = y) :
f x = f y

Deprecated: use FunLike.congr_arg instead.

@[deprecated]
theorem ZeroHom.coe_inj {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] ⦃f : ZeroHom M N ⦃g : ZeroHom M N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem OneHom.coe_inj {M : Type u_3} {N : Type u_4} [One M] [One N] ⦃f : OneHom M N ⦃g : OneHom M N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem AddHom.coe_inj {M : Type u_3} {N : Type u_4} [Add M] [Add N] ⦃f : AddHom M N ⦃g : AddHom M N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem MulHom.coe_inj {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] ⦃f : M →ₙ* N ⦃g : M →ₙ* N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem AddMonoidHom.coe_inj {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →+ N ⦃g : M →+ N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem MonoidHom.coe_inj {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →* N ⦃g : M →* N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem MonoidWithZeroHom.coe_inj {M : Type u_3} {N : Type u_4} [] [] ⦃f : M →*₀ N ⦃g : M →*₀ N (h : f = g) :
f = g

Deprecated: use FunLike.coe_injective instead.

@[deprecated]
theorem ZeroHom.ext_iff {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {f : ZeroHom M N} {g : ZeroHom M N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem OneHom.ext_iff {M : Type u_3} {N : Type u_4} [One M] [One N] {f : OneHom M N} {g : OneHom M N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem AddHom.ext_iff {M : Type u_3} {N : Type u_4} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem MulHom.ext_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem AddMonoidHom.ext_iff {M : Type u_3} {N : Type u_4} [] [] {f : M →+ N} {g : M →+ N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem MonoidHom.ext_iff {M : Type u_3} {N : Type u_4} [] [] {f : M →* N} {g : M →* N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[deprecated]
theorem MonoidWithZeroHom.ext_iff {M : Type u_3} {N : Type u_4} [] [] {f : M →*₀ N} {g : M →*₀ N} :
f = g ∀ (x : M), f x = g x

Deprecated: use FunLike.ext_iff instead.

@[simp]
theorem ZeroHom.mk_coe {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) (h1 : f 0 = 0) :
{ toFun := f, map_zero' := h1 } = f
@[simp]
theorem OneHom.mk_coe {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) (h1 : f 1 = 1) :
{ toFun := f, map_one' := h1 } = f
@[simp]
theorem AddHom.mk_coe {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{ toFun := f, map_add' := hmul } = f
@[simp]
theorem MulHom.mk_coe {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) (hmul : ∀ (x y : M), f (x * y) = f x * f y) :
{ toFun := f, map_mul' := hmul } = f
@[simp]
theorem AddMonoidHom.mk_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (hmul : ∀ (x y : M), ZeroHom.toFun (f) (x + y) = ZeroHom.toFun (f) x + ZeroHom.toFun (f) y) :
{ toZeroHom := f, map_add' := hmul } = f
@[simp]
theorem MonoidHom.mk_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) (hmul : ∀ (x y : M), OneHom.toFun (f) (x * y) = OneHom.toFun (f) x * OneHom.toFun (f) y) :
{ toOneHom := f, map_mul' := hmul } = f
@[simp]
theorem MonoidWithZeroHom.mk_coe {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) (h1 : ZeroHom.toFun (f) 1 = 1) (hmul : ∀ (x y : M), ZeroHom.toFun (f) (x * y) = ZeroHom.toFun (f) x * ZeroHom.toFun (f) y) :
{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = f
theorem ZeroHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) (f' : MN) (h : f' = f) :
f' 0 = 0
def ZeroHom.copy {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) (f' : MN) (h : f' = f) :

Copy of a ZeroHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
Instances For
def OneHom.copy {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) (f' : MN) (h : f' = f) :
OneHom M N

Copy of a OneHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
Instances For
@[simp]
theorem ZeroHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : MN) (h : f' = f), (ZeroHom.copy f f' h) = f'
@[simp]
theorem OneHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : MN) (h : f' = f), (OneHom.copy f f' h) = f'
theorem ZeroHom.coe_copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : MN) (h : f' = f), ZeroHom.copy f f' h = f
theorem OneHom.coe_copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : MN) (h : f' = f), OneHom.copy f f' h = f
theorem AddHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (f' : MN) (h : f' = f) (x : M) (y : M) :
f' (x + y) = f' x + f' y
def AddHom.copy {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) (f' : MN) (h : f' = f) :

Copy of an AddHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• AddHom.copy f f' h = { toFun := f', map_add' := (_ : ∀ (x y : M), f' (x + y) = f' x + f' y) }
Instances For
def MulHom.copy {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) (f' : MN) (h : f' = f) :

Copy of a MulHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• MulHom.copy f f' h = { toFun := f', map_mul' := (_ : ∀ (x y : M), f' (x * y) = f' x * f' y) }
Instances For
@[simp]
theorem AddHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : MN) (h : f' = f), (AddHom.copy f f' h) = f'
@[simp]
theorem MulHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : MN) (h : f' = f), (MulHom.copy f f' h) = f'
theorem AddHom.coe_copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : MN) (h : f' = f), AddHom.copy f f' h = f
theorem MulHom.coe_copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : MN) (h : f' = f), MulHom.copy f f' h = f
def AddMonoidHom.copy {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (f' : MN) (h : f' = f) :
M →+ N

Copy of an AddMonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidHom.copy.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (f' : MN) (h : f' = f) (x : M) (y : M) :
AddHom.toFun (AddHom.copy (f) f' h) (x + y) = AddHom.toFun (AddHom.copy (f) f' h) x + AddHom.toFun (AddHom.copy (f) f' h) y
theorem AddMonoidHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (f' : MN) (h : f' = f) :
ZeroHom.toFun (ZeroHom.copy (f) f' h) 0 = 0
def MonoidHom.copy {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) (f' : MN) (h : f' = f) :
M →* N

Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddMonoidHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →+ N) (f' : MN) (h : f' = f), () = f'
@[simp]
theorem MonoidHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →* N) (f' : MN) (h : f' = f), (MonoidHom.copy f f' h) = f'
theorem AddMonoidHom.copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →+ N) (f' : MN) (h : f' = f), = f
theorem MonoidHom.copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →* N) (f' : MN) (h : f' = f), MonoidHom.copy f f' h = f
def MonoidWithZeroHom.copy {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) (f' : MN) (h : f' = f) :
M →* N

Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonoidWithZeroHom.coe_copy {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →*₀ N) (f' : MN) (h : f' = f), () = f'
theorem MonoidWithZeroHom.copy_eq {M : Type u_3} {N : Type u_4} :
∀ {x : } {x_1 : } (f : M →*₀ N) (f' : MN) (h : f' = f), = f
theorem ZeroHom.map_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) :
f 0 = 0
theorem OneHom.map_one {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) :
f 1 = 1
theorem AddMonoidHom.map_zero {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
f 0 = 0

If f is an additive monoid homomorphism then f 0 = 0.

theorem MonoidHom.map_one {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
f 1 = 1

If f is a monoid homomorphism then f 1 = 1.

theorem MonoidWithZeroHom.map_one {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
f 1 = 1
theorem MonoidWithZeroHom.map_zero {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
f 0 = 0
theorem AddHom.map_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) (a : M) (b : M) :
f (a + b) = f a + f b
theorem MulHom.map_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) (a : M) (b : M) :
f (a * b) = f a * f b
theorem AddMonoidHom.map_add {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (a : M) (b : M) :
f (a + b) = f a + f b

If f is an additive monoid homomorphism then f (a + b) = f a + f b.

theorem MonoidHom.map_mul {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) (a : M) (b : M) :
f (a * b) = f a * f b

If f is a monoid homomorphism then f (a * b) = f a * f b.

theorem MonoidWithZeroHom.map_mul {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) (a : M) (b : M) :
f (a * b) = f a * f b
theorem AddMonoidHom.map_exists_right_neg {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {x : M} (hx : ∃ (y : M), x + y = 0) :
∃ (y : N), f x + y = 0

Given an AddMonoid homomorphism f : M →+ N and an element x : M, if x has a right inverse, then f x has a right inverse too.

abbrev AddMonoidHom.map_exists_right_neg.match_1 {M : Type u_1} [] {x : M} (motive : (∃ (y : M), x + y = 0)Prop) :
∀ (hx : ∃ (y : M), x + y = 0), (∀ (y : M) (hy : x + y = 0), motive (_ : ∃ (y : M), x + y = 0))motive hx
Equations
• (_ : motive hx) = (_ : motive hx)
Instances For
theorem MonoidHom.map_exists_right_inv {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {x : M} (hx : ∃ (y : M), x * y = 1) :
∃ (y : N), f x * y = 1

Given a monoid homomorphism f : M →* N and an element x : M, if x has a right inverse, then f x has a right inverse too. For elements invertible on both sides see IsUnit.map.

theorem AddMonoidHom.map_exists_left_neg {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {x : M} (hx : ∃ (y : M), y + x = 0) :
∃ (y : N), y + f x = 0

Given an AddMonoid homomorphism f : M →+ N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsAddUnit.map.

abbrev AddMonoidHom.map_exists_left_neg.match_1 {M : Type u_1} [] {x : M} (motive : (∃ (y : M), y + x = 0)Prop) :
∀ (hx : ∃ (y : M), y + x = 0), (∀ (y : M) (hy : y + x = 0), motive (_ : ∃ (y : M), y + x = 0))motive hx
Equations
• (_ : motive hx) = (_ : motive hx)
Instances For
theorem MonoidHom.map_exists_left_inv {M : Type u_3} {N : Type u_4} {F : Type u_8} [] [] [] (f : F) {x : M} (hx : ∃ (y : M), y * x = 1) :
∃ (y : N), y * f x = 1

Given a monoid homomorphism f : M →* N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsUnit.map.

theorem ZeroHom.id.proof_1 (M : Type u_1) [Zero M] :
(fun (x : M) => x) 0 = (fun (x : M) => x) 0
def ZeroHom.id (M : Type u_9) [Zero M] :

The identity map from a type with zero to itself.

Equations
• = { toFun := fun (x : M) => x, map_zero' := (_ : (fun (x : M) => x) 0 = (fun (x : M) => x) 0) }
Instances For
@[simp]
theorem OneHom.id_apply (M : Type u_9) [One M] (x : M) :
() x = x
@[simp]
theorem ZeroHom.id_apply (M : Type u_9) [Zero M] (x : M) :
() x = x
def OneHom.id (M : Type u_9) [One M] :
OneHom M M

The identity map from a type with 1 to itself.

Equations
• = { toFun := fun (x : M) => x, map_one' := (_ : (fun (x : M) => x) 1 = (fun (x : M) => x) 1) }
Instances For
def AddHom.id (M : Type u_9) [Add M] :

The identity map from a type with addition to itself.

Equations
• = { toFun := fun (x : M) => x, map_add' := (_ : ∀ (x x_1 : M), (fun (x : M) => x) (x + x_1) = (fun (x : M) => x) (x + x_1)) }
Instances For
theorem AddHom.id.proof_1 (M : Type u_1) [Add M] :
∀ (x x_1 : M), (fun (x : M) => x) (x + x_1) = (fun (x : M) => x) (x + x_1)
@[simp]
theorem AddHom.id_apply (M : Type u_9) [Add M] (x : M) :
() x = x
@[simp]
theorem MulHom.id_apply (M : Type u_9) [Mul M] (x : M) :
() x = x
def MulHom.id (M : Type u_9) [Mul M] :

The identity map from a type with multiplication to itself.

Equations
• = { toFun := fun (x : M) => x, map_mul' := (_ : ∀ (x x_1 : M), (fun (x : M) => x) (x * x_1) = (fun (x : M) => x) (x * x_1)) }
Instances For
theorem AddMonoidHom.id.proof_2 (M : Type u_1) [] :
∀ (x x_1 : M), ZeroHom.toFun { toFun := fun (x : M) => x, map_zero' := (_ : (fun (x : M) => x) 0 = (fun (x : M) => x) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun (x : M) => x, map_zero' := (_ : (fun (x : M) => x) 0 = (fun (x : M) => x) 0) } (x + x_1)
theorem AddMonoidHom.id.proof_1 (M : Type u_1) [] :
(fun (x : M) => x) 0 = (fun (x : M) => x) 0
def AddMonoidHom.id (M : Type u_9) [] :
M →+ M

The identity map from an additive monoid to itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddMonoidHom.id_apply (M : Type u_9) [] (x : M) :
() x = x
@[simp]
theorem MonoidHom.id_apply (M : Type u_9) [] (x : M) :
() x = x
def MonoidHom.id (M : Type u_9) [] :
M →* M

The identity map from a monoid to itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonoidWithZeroHom.id_apply (M : Type u_9) [] (x : M) :
x = x
def MonoidWithZeroHom.id (M : Type u_9) [] :

The identity map from a MonoidWithZero to itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ZeroHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Zero M] [Zero N] [Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :
hnp (hmn 0) = 0
def ZeroHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :

Composition of ZeroHoms as a ZeroHom.

Equations
• ZeroHom.comp hnp hmn = { toFun := hnp hmn, map_zero' := (_ : hnp (hmn 0) = 0) }
Instances For
def OneHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) :
OneHom M P

Composition of OneHoms as a OneHom.

Equations
• OneHom.comp hnp hmn = { toFun := hnp hmn, map_one' := (_ : hnp (hmn 1) = 1) }
Instances For
def AddHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (hnp : AddHom N P) (hmn : AddHom M N) :

Composition of AddHoms as an AddHom.

Equations
• AddHom.comp hnp hmn = { toFun := hnp hmn, map_add' := (_ : ∀ (x y : M), hnp (hmn (x + y)) = hnp (hmn x) + hnp (hmn y)) }
Instances For
theorem AddHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [Add P] (hnp : AddHom N P) (hmn : AddHom M N) (x : M) (y : M) :
hnp (hmn (x + y)) = hnp (hmn x) + hnp (hmn y)
def MulHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) :

Composition of MulHoms as a MulHom.

Equations
• MulHom.comp hnp hmn = { toFun := hnp hmn, map_mul' := (_ : ∀ (x y : M), hnp (hmn (x * y)) = hnp (hmn x) * hnp (hmn y)) }
Instances For
def AddMonoidHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (hnp : N →+ P) (hmn : M →+ N) :
M →+ P

Composition of additive monoid morphisms as an additive monoid morphism.

Equations
• AddMonoidHom.comp hnp hmn = { toZeroHom := { toFun := hnp hmn, map_zero' := (_ : hnp (hmn 0) = 0) }, map_add' := (_ : ∀ (a a_1 : M), hnp (hmn (a + a_1)) = hnp (hmn a) + hnp (hmn a_1)) }
Instances For
theorem AddMonoidHom.comp.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [] [] [] (hnp : N →+ P) (hmn : M →+ N) (a : M) (a : M) :
hnp (hmn (a✝ + a)) = hnp (hmn a✝) + hnp (hmn a)
theorem AddMonoidHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [] [] [] (hnp : N →+ P) (hmn : M →+ N) :
hnp (hmn 0) = 0
def MonoidHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (hnp : N →* P) (hmn : M →* N) :
M →* P

Composition of monoid morphisms as a monoid morphism.

Equations
• MonoidHom.comp hnp hmn = { toOneHom := { toFun := hnp hmn, map_one' := (_ : hnp (hmn 1) = 1) }, map_mul' := (_ : ∀ (a a_1 : M), hnp (hmn (a * a_1)) = hnp (hmn a) * hnp (hmn a_1)) }
Instances For
def MonoidWithZeroHom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (hnp : N →*₀ P) (hmn : M →*₀ N) :

Composition of MonoidWithZeroHoms as a MonoidWithZeroHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ZeroHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (g : ZeroHom N P) (f : ZeroHom M N) :
() = g f
@[simp]
theorem OneHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) :
() = g f
@[simp]
theorem AddHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) :
() = g f
@[simp]
theorem MulHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
() = g f
@[simp]
theorem AddMonoidHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →+ P) (f : M →+ N) :
() = g f
@[simp]
theorem MonoidHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →* P) (f : M →* N) :
() = g f
@[simp]
theorem MonoidWithZeroHom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →*₀ P) (f : M →*₀ N) :
() = g f
theorem ZeroHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (g : ZeroHom N P) (f : ZeroHom M N) (x : M) :
() x = g (f x)
theorem OneHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) :
() x = g (f x)
theorem AddHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) (x : M) :
() x = g (f x)
theorem MulHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) (x : M) :
() x = g (f x)
theorem AddMonoidHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →+ P) (f : M →+ N) (x : M) :
() x = g (f x)
theorem MonoidHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →* P) (f : M →* N) (x : M) :
() x = g (f x)
theorem MonoidWithZeroHom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →*₀ P) (f : M →*₀ N) (x : M) :
() x = g (f x)
theorem ZeroHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [Zero M] [Zero N] [Zero P] [Zero Q] (f : ZeroHom M N) (g : ZeroHom N P) (h : ZeroHom P Q) :

Composition of additive monoid homomorphisms is associative.

theorem OneHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [One M] [One N] [One P] [One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :

Composition of monoid homomorphisms is associative.

theorem AddHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [Add M] [Add N] [Add P] [Add Q] (f : AddHom M N) (g : AddHom N P) (h : AddHom P Q) :
theorem MulHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [Mul M] [Mul N] [Mul P] [Mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :
theorem AddMonoidHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [] [] [] [] (f : M →+ N) (g : N →+ P) (h : P →+ Q) :
=
theorem MonoidHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [] [] [] [] (f : M →* N) (g : N →* P) (h : P →* Q) :
theorem MonoidWithZeroHom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_9} [] [] [] [] (f : M →*₀ N) (g : N →*₀ P) (h : P →*₀ Q) :
theorem ZeroHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] {g₁ : ZeroHom N P} {g₂ : ZeroHom N P} {f : ZeroHom M N} (hf : ) :
ZeroHom.comp g₁ f = ZeroHom.comp g₂ f g₁ = g₂
theorem OneHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] {g₁ : OneHom N P} {g₂ : OneHom N P} {f : OneHom M N} (hf : ) :
OneHom.comp g₁ f = OneHom.comp g₂ f g₁ = g₂
theorem AddHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] {g₁ : AddHom N P} {g₂ : AddHom N P} {f : AddHom M N} (hf : ) :
AddHom.comp g₁ f = AddHom.comp g₂ f g₁ = g₂
theorem MulHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] {g₁ : N →ₙ* P} {g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : ) :
MulHom.comp g₁ f = MulHom.comp g₂ f g₁ = g₂
theorem AddMonoidHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g₁ : N →+ P} {g₂ : N →+ P} {f : M →+ N} (hf : ) :
= g₁ = g₂
theorem MonoidHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g₁ : N →* P} {g₂ : N →* P} {f : M →* N} (hf : ) :
= g₁ = g₂
theorem MonoidWithZeroHom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g₁ : N →*₀ P} {g₂ : N →*₀ P} {f : M →*₀ N} (hf : ) :
g₁ = g₂
theorem ZeroHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] {g : ZeroHom N P} {f₁ : ZeroHom M N} {f₂ : ZeroHom M N} (hg : ) :
ZeroHom.comp g f₁ = ZeroHom.comp g f₂ f₁ = f₂
theorem OneHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] {g : OneHom N P} {f₁ : OneHom M N} {f₂ : OneHom M N} (hg : ) :
OneHom.comp g f₁ = OneHom.comp g f₂ f₁ = f₂
theorem AddHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] {g : AddHom N P} {f₁ : AddHom M N} {f₂ : AddHom M N} (hg : ) :
AddHom.comp g f₁ = AddHom.comp g f₂ f₁ = f₂
theorem MulHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ : M →ₙ* N} {f₂ : M →ₙ* N} (hg : ) :
MulHom.comp g f₁ = MulHom.comp g f₂ f₁ = f₂
theorem AddMonoidHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g : N →+ P} {f₁ : M →+ N} {f₂ : M →+ N} (hg : ) :
= f₁ = f₂
theorem MonoidHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g : N →* P} {f₁ : M →* N} {f₂ : M →* N} (hg : ) :
= f₁ = f₂
theorem MonoidWithZeroHom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] {g : N →*₀ P} {f₁ : M →*₀ N} {f₂ : M →*₀ N} (hg : ) :
f₁ = f₂
theorem AddMonoidHom.toZeroHom_injective {M : Type u_3} {N : Type u_4} [] [] :
theorem MonoidHom.toOneHom_injective {M : Type u_3} {N : Type u_4} [] [] :
Function.Injective MonoidHom.toOneHom
theorem AddMonoidHom.toAddHom_injective {M : Type u_3} {N : Type u_4} [] [] :
theorem MonoidHom.toMulHom_injective {M : Type u_3} {N : Type u_4} [] [] :
Function.Injective MonoidHom.toMulHom
theorem MonoidWithZeroHom.toMonoidHom_injective {M : Type u_3} {N : Type u_4} [] [] :
Function.Injective MonoidWithZeroHom.toMonoidHom
theorem MonoidWithZeroHom.toZeroHom_injective {M : Type u_3} {N : Type u_4} [] [] :
Function.Injective MonoidWithZeroHom.toZeroHom
@[simp]
theorem ZeroHom.comp_id {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) :
= f
@[simp]
theorem OneHom.comp_id {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) :
OneHom.comp f () = f
@[simp]
theorem AddHom.comp_id {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) :
AddHom.comp f () = f
@[simp]
theorem MulHom.comp_id {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) :
MulHom.comp f () = f
@[simp]
theorem AddMonoidHom.comp_id {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
@[simp]
theorem MonoidHom.comp_id {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
= f
@[simp]
theorem MonoidWithZeroHom.comp_id {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
@[simp]
theorem ZeroHom.id_comp {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) :
= f
@[simp]
theorem OneHom.id_comp {M : Type u_3} {N : Type u_4} [One M] [One N] (f : OneHom M N) :
OneHom.comp () f = f
@[simp]
theorem AddHom.id_comp {M : Type u_3} {N : Type u_4} [Add M] [Add N] (f : AddHom M N) :
AddHom.comp () f = f
@[simp]
theorem MulHom.id_comp {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (f : M →ₙ* N) :
MulHom.comp () f = f
@[simp]
theorem AddMonoidHom.id_comp {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) :
@[simp]
theorem MonoidHom.id_comp {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) :
= f
@[simp]
theorem MonoidWithZeroHom.id_comp {M : Type u_3} {N : Type u_4} [] [] (f : M →*₀ N) :
theorem AddMonoidHom.map_nsmul {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (a : M) (n : ) :
f (n a) = n f a
theorem MonoidHom.map_pow {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) (a : M) (n : ) :
f (a ^ n) = f a ^ n
theorem AddMonoidHom.map_zsmul' {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (hf : ∀ (x : M), f (-x) = -f x) (a : M) (n : ) :
f (n a) = n f a
theorem MonoidHom.map_zpow' {M : Type u_3} {N : Type u_4} [] [] (f : M →* N) (hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹) (a : M) (n : ) :
f (a ^ n) = f a ^ n
def Monoid.End (M : Type u_3) [] :
Type u_3

The monoid of endomorphisms.

Equations
Instances For
instance Monoid.End.instMonoidEnd (M : Type u_3) [] :
Equations
instance Monoid.End.instInhabitedEnd (M : Type u_3) [] :
Equations
• = { default := 1 }
Equations
• = MonoidHom.monoidHomClass
@[simp]
theorem Monoid.coe_one (M : Type u_3) [] :
1 = id
@[simp]
theorem Monoid.coe_mul (M : Type u_3) [] (f : ) (g : ) :
(f * g) = f g
def AddMonoid.End (A : Type u_9) [] :
Type u_9

The monoid of endomorphisms.

Equations
Instances For
instance AddMonoid.End.monoid (A : Type u_9) [] :
Equations
instance AddMonoid.End.instInhabitedEnd (A : Type u_9) [] :
Equations
• = { default := 1 }
Equations
@[simp]
theorem AddMonoid.coe_one (A : Type u_9) [] :
1 = id
@[simp]
theorem AddMonoid.coe_mul (A : Type u_9) [] (f : ) (g : ) :
(f * g) = f g
theorem instZeroZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] :
(fun (x : M) => 0) 0 = (fun (x : M) => 0) 0
instance instZeroZeroHom {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :

0 is the homomorphism sending all elements to 0.

Equations
• instZeroZeroHom = { zero := { toFun := fun (x : M) => 0, map_zero' := (_ : (fun (x : M) => 0) 0 = (fun (x : M) => 0) 0) } }
instance instOneOneHom {M : Type u_3} {N : Type u_4} [One M] [One N] :
One (OneHom M N)

1 is the homomorphism sending all elements to 1.

Equations
• instOneOneHom = { one := { toFun := fun (x : M) => 1, map_one' := (_ : (fun (x : M) => 1) 1 = (fun (x : M) => 1) 1) } }
instance instZeroAddHomToAdd {M : Type u_3} {N : Type u_4} [Add M] [] :
Zero (AddHom M N)

0 is the additive homomorphism sending all elements to 0

Equations
• instZeroAddHomToAdd = { zero := { toFun := fun (x : M) => 0, map_add' := (_ : MM0 = 0 + 0) } }
theorem instZeroAddHomToAdd.proof_1 {M : Type u_2} {N : Type u_1} [] :
MM0 = 0 + 0
instance instOneMulHomToMul {M : Type u_3} {N : Type u_4} [Mul M] [] :
One (M →ₙ* N)

1 is the multiplicative homomorphism sending all elements to 1.

Equations
• instOneMulHomToMul = { one := { toFun := fun (x : M) => 1, map_mul' := (_ : MM1 = 1 * 1) } }
theorem instZeroAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} [] :
MM0 = 0 + 0
instance instZeroAddMonoidHom {M : Type u_3} {N : Type u_4} [] [] :
Zero (M →+ N)

0 is the additive monoid homomorphism sending all elements to 0.

Equations
• One or more equations did not get rendered due to their size.
theorem instZeroAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [] [] :
(fun (x : M) => 0) 0 = (fun (x : M) => 0) 0
instance instOneMonoidHom {M : Type u_3} {N : Type u_4} [] [] :
One (M →* N)

1 is the monoid homomorphism sending all elements to 1.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem ZeroHom.zero_apply {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (x : M) :
0 x = 0
@[simp]
theorem OneHom.one_apply {M : Type u_3} {N : Type u_4} [One M] [One N] (x : M) :
1 x = 1
@[simp]
theorem AddMonoidHom.zero_apply {M : Type u_3} {N : Type u_4} [] [] (x : M) :
0 x = 0
@[simp]
theorem MonoidHom.one_apply {M : Type u_3} {N : Type u_4} [] [] (x : M) :
1 x = 1
@[simp]
theorem ZeroHom.zero_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (f : ZeroHom M N) :
= 0
@[simp]
theorem OneHom.one_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (f : OneHom M N) :
= 1
@[simp]
theorem ZeroHom.comp_zero {M : Type u_3} {N : Type u_4} {P : Type u_5} [Zero M] [Zero N] [Zero P] (f : ZeroHom N P) :
= 0
@[simp]
theorem OneHom.comp_one {M : Type u_3} {N : Type u_4} {P : Type u_5} [One M] [One N] [One P] (f : OneHom N P) :
= 1
instance instInhabitedZeroHom {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
Equations
• instInhabitedZeroHom = { default := 0 }
instance instInhabitedOneHom {M : Type u_3} {N : Type u_4} [One M] [One N] :
Equations
• instInhabitedOneHom = { default := 1 }
instance instInhabitedAddHomToAdd {M : Type u_3} {N : Type u_4} [Add M] [] :
Equations
• instInhabitedAddHomToAdd = { default := 0 }
instance instInhabitedMulHomToMul {M : Type u_3} {N : Type u_4} [Mul M] [] :
Equations
• instInhabitedMulHomToMul = { default := 1 }
instance instInhabitedAddMonoidHom {M : Type u_3} {N : Type u_4} [] [] :
Equations
• instInhabitedAddMonoidHom = { default := 0 }
instance instInhabitedMonoidHom {M : Type u_3} {N : Type u_4} [] [] :
Equations
• instInhabitedMonoidHom = { default := 1 }
Equations
• instInhabitedMonoidWithZeroHom = { default := }
@[simp]
theorem AddMonoidHom.zero_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (f : M →+ N) :
= 0
@[simp]
theorem MonoidHom.one_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (f : M →* N) :
= 1
@[simp]
theorem AddMonoidHom.comp_zero {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (f : N →+ P) :
= 0
@[simp]
theorem MonoidHom.comp_one {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (f : N →* P) :
= 1
theorem AddMonoidHom.map_neg {α : Type u_1} {β : Type u_2} [] (f : α →+ β) (a : α) :
f (-a) = -f a

Additive group homomorphisms preserve negation.

theorem MonoidHom.map_inv {α : Type u_1} {β : Type u_2} [] [] (f : α →* β) (a : α) :
f a⁻¹ = (f a)⁻¹

Group homomorphisms preserve inverse.

theorem AddMonoidHom.map_zsmul {α : Type u_1} {β : Type u_2} [] (f : α →+ β) (g : α) (n : ) :
f (n g) = n f g

Additive group homomorphisms preserve integer scaling.

theorem MonoidHom.map_zpow {α : Type u_1} {β : Type u_2} [] [] (f : α →* β) (g : α) (n : ) :
f (g ^ n) = f g ^ n

Group homomorphisms preserve integer power.

theorem AddMonoidHom.map_sub {α : Type u_1} {β : Type u_2} [] (f : α →+ β) (g : α) (h : α) :
f (g - h) = f g - f h

Additive group homomorphisms preserve subtraction.

theorem MonoidHom.map_div {α : Type u_1} {β : Type u_2} [] [] (f : α →* β) (g : α) (h : α) :
f (g / h) = f g / f h

Group homomorphisms preserve division.

theorem AddMonoidHom.map_add_neg {α : Type u_1} {β : Type u_2} [] (f : α →+ β) (g : α) (h : α) :
f (g + -h) = f g + -f h

Additive group homomorphisms preserve subtraction.

theorem MonoidHom.map_mul_inv {α : Type u_1} {β : Type u_2} [] [] (f : α →* β) (g : α) (h : α) :
f (g * h⁻¹) = f g * (f h)⁻¹

Group homomorphisms preserve division.