# mathlibdocumentation

algebra.group.hom

# monoid and group homomorphisms #

This file defines the bundled structures for monoid and group homomorphisms. Namely, we define `monoid_hom` (resp., `add_monoid_hom`) 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:

• `zero_hom`
• `one_hom`
• `add_hom`
• `mul_hom`
• `monoid_with_zero_hom`

## Notations #

• `→*` for bundled monoid homs (also use for group homs)
• `→+` for bundled add_monoid homs (also use for add_group 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 `group_hom` -- the idea is that `monoid_hom` is used. The constructor for `monoid_hom` needs a proof of `map_one` as well as `map_mul`; a separate constructor `monoid_hom.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 `monoid_hom`. 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 zero_hom (M : Type u_7) (N : Type u_8) [has_zero M] [has_zero N] :
Type (max u_7 u_8)
• to_fun : M → N
• map_zero' : self.to_fun 0 = 0

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

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

When you extend this structure, make sure to also extend `zero_hom_class`.

@[instance]
def zero_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_zero M] [has_zero N] [self : N] :
M (λ (_x : M), N)
@[class]
structure zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_zero M] [has_zero N] :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_zero : ∀ (f : F), f 0 = 0

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

You should extend this typeclass when you extend `zero_hom`.

Instances
Type (max u_7 u_8)

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

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

When you extend this structure, make sure to extend `add_hom_class`.

@[class]
structure add_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_add M] [has_add N] :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

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

Instances
@[instance]
def add_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_add M] [has_add N] [self : N] :
M (λ (_x : M), N)
@[nolint]
def add_monoid_hom.to_add_hom {M : Type u_7} {N : Type u_8} (self : M →+ N) :
N
structure add_monoid_hom (M : Type u_7) (N : Type u_8)  :
Type (max u_7 u_8)

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

`add_monoid_hom` is also used for group homomorphisms.

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

When you extend this structure, make sure to extend `add_monoid_hom_class`.

@[nolint]
def add_monoid_hom.to_zero_hom {M : Type u_7} {N : Type u_8} (self : M →+ N) :
N
@[class]
structure add_monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0

`add_monoid_hom_class F M N` states that `F` is a type of `add_zero_class`-preserving homomorphisms.

You should also extend this typeclass when you extend `add_monoid_hom`.

Instances
@[instance]
def add_monoid_hom_class.to_add_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
@[instance]
def add_monoid_hom_class.to_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
structure one_hom (M : Type u_7) (N : Type u_8) [has_one M] [has_one N] :
Type (max u_7 u_8)
• to_fun : M → N
• map_one' : self.to_fun 1 = 1

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

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

When you extend this structure, make sure to also extend `one_hom_class`.

@[class]
structure one_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_one M] [has_one N] :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_one : ∀ (f : F), f 1 = 1

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

Instances
@[instance]
def one_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_one M] [has_one N] [self : N] :
M (λ (_x : M), N)
@[protected, instance]
def one_hom.one_hom_class {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :
Equations
@[protected, instance]
def zero_hom.zero_hom_class {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :
Equations
@[simp]
theorem map_one {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_one M] [has_one N] [ N] (f : F) :
f 1 = 1
@[simp]
theorem map_zero {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_zero M] [has_zero N] [ N] (f : F) :
f 0 = 0
theorem map_eq_one_iff {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_one M] [has_one N] [ N] (f : F) (hf : function.injective f) {x : M} :
f x = 1 x = 1
theorem map_eq_zero_iff {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_zero M] [has_zero N] [ N] (f : F) (hf : function.injective f) {x : M} :
f x = 0 x = 0
structure mul_hom (M : Type u_7) (N : Type u_8) [has_mul M] [has_mul N] :
Type (max u_7 u_8)

`mul_hom M N` is the type of functions `M → N` that preserve multiplication.

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

@[instance]
def mul_hom_class.to_fun_like (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_mul M] [has_mul N] [self : N] :
M (λ (_x : M), N)
@[class]
structure mul_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [has_mul M] [has_mul N] :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_mul : ∀ (f : F) (x y : M), f (x * y) = (f x) * f y

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

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

Instances
@[protected, instance]
Equations
@[protected, instance]
def mul_hom.mul_hom_class {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
Equations
@[simp]
theorem map_add {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] [ N] (f : F) (x y : M) :
f (x + y) = f x + f y
@[simp]
theorem map_mul {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] [ N] (f : F) (x y : M) :
f (x * y) = (f x) * f y
structure monoid_hom (M : Type u_7) (N : Type u_8)  :
Type (max u_7 u_8)

`M →* N` is the type of functions `M → N` that preserve the `monoid` structure. `monoid_hom` is also used for group homomorphisms.

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

When you extend this structure, make sure to extend `monoid_hom_class`.

@[nolint]
def monoid_hom.to_one_hom {M : Type u_7} {N : Type u_8} (self : M →* N) :
N
@[nolint]
def monoid_hom.to_mul_hom {M : Type u_7} {N : Type u_8} (self : M →* N) :
N
@[class]
structure monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• map_mul : ∀ (f : F) (x y : M), f (x * y) = (f x) * f y
• map_one : ∀ (f : F), f 1 = 1

`monoid_hom_class F M N` states that `F` is a type of `monoid`-preserving homomorphisms. You should also extend this typeclass when you extend `monoid_hom`.

Instances
@[instance]
def monoid_hom_class.to_one_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
@[instance]
def monoid_hom_class.to_mul_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
@[protected, instance]
Equations
@[protected, instance]
def monoid_hom.monoid_hom_class {M : Type u_1} {N : Type u_2}  :
Equations
@[protected, instance]
def add_monoid_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [ N] :
(M →+ N)
Equations
@[protected, instance]
def monoid_hom.has_coe_t {M : Type u_1} {N : Type u_2} {F : Type u_6} [ N] :
(M →* N)
Equations
theorem map_mul_eq_one {M : Type u_1} {N : Type u_2} {F : Type u_6} [ N] (f : F) {a b : M} (h : a * b = 1) :
(f a) * f b = 1
theorem map_add_eq_zero {M : Type u_1} {N : Type u_2} {F : Type u_6} [ N] (f : F) {a b : M} (h : a + b = 0) :
f a + f b = 0
@[simp]
theorem map_inv {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [ H] (f : F) (g : G) :

Group homomorphisms preserve inverse.

@[simp]
theorem map_neg {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [ H] (f : F) (g : G) :
f (-g) = -f g
@[simp]
theorem map_mul_inv {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [ H] (f : F) (g h : G) :
f (g * h⁻¹) = (f g) * (f h)⁻¹

Group homomorphisms preserve division.

@[simp]
theorem map_add_neg {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [ H] (f : F) (g h : G) :
f (g + -h) = f g + -f h
@[simp]
theorem map_div {G : Type u_4} {H : Type u_5} {F : Type u_6} [group G] [group H] [ H] (f : F) (x y : G) :
f (x / y) = f x / f y

Group homomorphisms preserve division.

@[simp]
theorem map_sub {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [ H] (f : F) (x y : G) :
f (x - y) = f x - f y
@[simp]
theorem map_pow {G : Type u_4} {H : Type u_5} {F : Type u_6} [monoid G] [monoid H] [ H] (f : F) (a : G) (n : ) :
f (a ^ n) = f a ^ n
@[simp]
theorem map_nsmul {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_monoid G] [add_monoid H] [ H] (f : F) (a : G) (n : ) :
f (n a) = n f a
theorem map_zpow' {G : Type u_4} {H : Type u_5} {F : Type u_6} [ H] (f : F) (hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹) (a : G) (n : ) :
f (a ^ n) = f a ^ n
theorem map_zsmul' {G : Type u_4} {H : Type u_5} {F : Type u_6} [ H] (f : F) (hf : ∀ (x : G), f (-x) = -f x) (a : G) (n : ) :
f (n a) = n f a
@[simp]
theorem map_zsmul {G : Type u_4} {H : Type u_5} {F : Type u_6} [add_group G] [add_group H] [ H] (f : F) (g : G) (n : ) :
f (n g) = n f g

Additive group homomorphisms preserve integer scaling.

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

Group homomorphisms preserve integer power.

@[nolint]
def monoid_with_zero_hom.to_zero_hom {M : Type u_7} {N : Type u_8} (self : N) :
N
structure monoid_with_zero_hom (M : Type u_7) (N : Type u_8)  :
Type (max u_7 u_8)

`monoid_with_zero_hom M N` is the type of functions `M → N` that preserve the `monoid_with_zero` structure.

`monoid_with_zero_hom` is also used for group homomorphisms.

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

When you extend this structure, make sure to extend `monoid_with_zero_hom_class`.

@[nolint]
def monoid_with_zero_hom.to_monoid_hom {M : Type u_7} {N : Type u_8} (self : N) :
M →* N
@[class]
structure monoid_with_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9))  :
Type (max u_7 u_8 u_9)
• coe : F → Π (a : M), (λ (_x : M), N) a
• coe_injective' :
• 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

`monoid_with_zero_hom_class F M N` states that `F` is a type of `monoid_with_zero`-preserving homomorphisms.

You should also extend this typeclass when you extend `monoid_with_zero_hom`.

Instances
@[instance]
def monoid_with_zero_hom_class.to_monoid_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
@[instance]
def monoid_with_zero_hom_class.to_zero_hom_class (F : Type u_7) (M : out_param (Type u_8)) (N : out_param (Type u_9)) [self : N] :
N
@[protected, instance]
def monoid_with_zero_hom.monoid_with_zero_hom_class {M : Type u_1} {N : Type u_2}  :
Equations

Bundled morphisms can be down-cast to weaker bundlings

@[protected, instance]
def add_monoid_hom.has_coe_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} :
has_coe (M →+ N) (zero_hom M N)
Equations
@[protected, instance]
def monoid_hom.has_coe_to_one_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe (M →* N) (one_hom M N)
Equations
@[protected, instance]
has_coe (M →+ N) (add_hom M N)
Equations
@[protected, instance]
def monoid_hom.has_coe_to_mul_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe (M →* N) (mul_hom M N)
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_monoid_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
(M →* N)
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
(zero_hom M N)
Equations

The simp-normal form of morphism coercion is `f.to_..._hom`. This choice is primarily because this is the way things were before the above coercions were introduced. Bundled morphisms defined elsewhere in Mathlib may choose `↑f` as their simp-normal form instead.

@[simp]
theorem add_monoid_hom.coe_eq_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) :
@[simp]
theorem monoid_hom.coe_eq_to_one_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :
@[simp]
theorem monoid_hom.coe_eq_to_mul_hom {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) :
@[simp]
theorem add_monoid_hom.coe_eq_to_add_hom {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) :
@[simp]
theorem monoid_with_zero_hom.coe_eq_to_monoid_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : N) :
@[simp]
theorem monoid_with_zero_hom.coe_eq_to_zero_hom {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : N) :
@[protected, instance]
def zero_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_zero M} {mN : has_zero N} :
has_coe_to_fun (zero_hom M N) (λ (_x : N), M → N)
Equations
@[protected, instance]
def one_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_one M} {mN : has_one N} :
has_coe_to_fun (one_hom M N) (λ (_x : N), M → N)
Equations
@[protected, instance]
def mul_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : has_mul N} :
has_coe_to_fun (mul_hom M N) (λ (_x : N), M → N)
Equations
@[protected, instance]
def add_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : has_add N} :
has_coe_to_fun (add_hom M N) (λ (_x : N), M → N)
Equations
@[protected, instance]
def monoid_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe_to_fun (M →* N) (λ (_x : M →* N), M → N)
Equations
@[protected, instance]
def add_monoid_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} :
has_coe_to_fun (M →+ N) (λ (_x : M →+ N), M → N)
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_fun {M : Type u_1} {N : Type u_2} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
(λ (_x : , M → N)
Equations
@[simp]
theorem zero_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) :
@[simp]
theorem add_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
theorem mul_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) :
@[simp]
theorem add_monoid_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_fun_eq_coe {M : Type u_1} {N : Type u_2} (f : N) :
@[simp]
theorem one_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : M → N) (h1 : f 1 = 1) :
{to_fun := f, map_one' := h1} = f
@[simp]
theorem zero_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : M → N) (h1 : f 0 = 0) :
{to_fun := f, map_zero' := h1} = f
@[simp]
theorem mul_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M → N) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_mul' := hmul} = f
@[simp]
theorem add_hom.coe_mk {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : M → N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_add' := hmul} = f
@[simp]
theorem add_monoid_hom.coe_mk {M : Type u_1} {N : Type u_2} (f : M → N) (h1 : f 0 = 0) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_zero' := h1, map_add' := hmul} = f
@[simp]
theorem monoid_hom.coe_mk {M : Type u_1} {N : Type u_2} (f : M → N) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_one' := h1, map_mul' := hmul} = f
@[simp]
theorem monoid_with_zero_hom.coe_mk {M : Type u_1} {N : Type u_2} (f : M → N) (h0 : f 0 = 0) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul} = f
@[simp]
theorem add_monoid_hom.to_zero_hom_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_one_hom_coe {M : Type u_1} {N : Type u_2} (f : M →* N) :
@[simp]
theorem add_monoid_hom.to_add_hom_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_mul_hom_coe {M : Type u_1} {N : Type u_2} (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_zero_hom_coe {M : Type u_1} {N : Type u_2} (f : N) :
@[simp]
theorem monoid_with_zero_hom.to_monoid_hom_coe {M : Type u_1} {N : Type u_2} (f : N) :
theorem zero_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] {f g : N} (h : f = g) (x : M) :
f x = g x
theorem one_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] {f g : N} (h : f = g) (x : M) :
f x = g x
theorem mul_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : N} (h : f = g) (x : M) :
f x = g x
theorem add_hom.congr_fun {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : N} (h : f = g) (x : M) :
f x = g x
theorem monoid_hom.congr_fun {M : Type u_1} {N : Type u_2} {f g : M →* N} (h : f = g) (x : M) :
f x = g x
theorem add_monoid_hom.congr_fun {M : Type u_1} {N : Type u_2} {f g : M →+ N} (h : f = g) (x : M) :
f x = g x
theorem monoid_with_zero_hom.congr_fun {M : Type u_1} {N : Type u_2} {f g : N} (h : f = g) (x : M) :
f x = g x
theorem one_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) {x y : M} (h : x = y) :
f x = f y
theorem zero_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) {x y : M} (h : x = y) :
f x = f y
theorem mul_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) {x y : M} (h : x = y) :
f x = f y
theorem add_hom.congr_arg {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) {x y : M} (h : x = y) :
f x = f y
theorem monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} (f : M →* N) {x y : M} (h : x = y) :
f x = f y
theorem add_monoid_hom.congr_arg {M : Type u_1} {N : Type u_2} (f : M →+ N) {x y : M} (h : x = y) :
f x = f y
theorem monoid_with_zero_hom.congr_arg {M : Type u_1} {N : Type u_2} (f : N) {x y : M} (h : x = y) :
f x = f y
theorem zero_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] ⦃f g : N⦄ (h : f = g) :
f = g
theorem one_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] ⦃f g : N⦄ (h : f = g) :
f = g
theorem add_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] ⦃f g : N⦄ (h : f = g) :
f = g
theorem mul_hom.coe_inj {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : N⦄ (h : f = g) :
f = g
theorem add_monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} ⦃f g : M →+ N⦄ (h : f = g) :
f = g
theorem monoid_hom.coe_inj {M : Type u_1} {N : Type u_2} ⦃f g : M →* N⦄ (h : f = g) :
f = g
theorem monoid_with_zero_hom.coe_inj {M : Type u_1} {N : Type u_2} ⦃f g : N⦄ (h : f = g) :
f = g
theorem zero_hom.ext {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] ⦃f g : N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem one_hom.ext {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] ⦃f g : N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem mul_hom.ext {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] ⦃f g : N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem add_hom.ext {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] ⦃f g : N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_hom.ext {M : Type u_1} {N : Type u_2} ⦃f g : M →* N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem add_monoid_hom.ext {M : Type u_1} {N : Type u_2} ⦃f g : M →+ N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_with_zero_hom.ext {M : Type u_1} {N : Type u_2} ⦃f g : N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem zero_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] {f g : N} :
f = g ∀ (x : M), f x = g x
theorem one_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] {f g : N} :
f = g ∀ (x : M), f x = g x
theorem add_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : N} :
f = g ∀ (x : M), f x = g x
theorem mul_hom.ext_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : N} :
f = g ∀ (x : M), f x = g x
theorem monoid_hom.ext_iff {M : Type u_1} {N : Type u_2} {f g : M →* N} :
f = g ∀ (x : M), f x = g x
theorem add_monoid_hom.ext_iff {M : Type u_1} {N : Type u_2} {f g : M →+ N} :
f = g ∀ (x : M), f x = g x
theorem monoid_with_zero_hom.ext_iff {M : Type u_1} {N : Type u_2} {f g : N} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem zero_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) (h1 : f 0 = 0) :
{to_fun := f, map_zero' := h1} = f
@[simp]
theorem one_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) (h1 : f 1 = 1) :
{to_fun := f, map_one' := h1} = f
@[simp]
theorem add_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_add' := hmul} = f
@[simp]
theorem mul_hom.mk_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_mul' := hmul} = f
@[simp]
theorem add_monoid_hom.mk_coe {M : Type u_1} {N : Type u_2} (f : M →+ N) (h1 : f 0 = 0) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, map_zero' := h1, map_add' := hmul} = f
@[simp]
theorem monoid_hom.mk_coe {M : Type u_1} {N : Type u_2} (f : M →* N) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_one' := h1, map_mul' := hmul} = f
@[simp]
theorem monoid_with_zero_hom.mk_coe {M : Type u_1} {N : Type u_2} (f : N) (h0 : f 0 = 0) (h1 : f 1 = 1) (hmul : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul} = f
@[protected]
theorem one_hom.map_one {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) :
f 1 = 1
@[protected]
theorem zero_hom.map_zero {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) :
f 0 = 0
@[protected]
theorem add_monoid_hom.map_zero {M : Type u_1} {N : Type u_2} (f : M →+ N) :
f 0 = 0

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

@[protected]
theorem monoid_hom.map_one {M : Type u_1} {N : Type u_2} (f : M →* N) :
f 1 = 1

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

@[protected]
theorem monoid_with_zero_hom.map_one {M : Type u_1} {N : Type u_2} (f : N) :
f 1 = 1
@[protected]
theorem monoid_with_zero_hom.map_zero {M : Type u_1} {N : Type u_2} (f : N) :
f 0 = 0
@[protected]
theorem mul_hom.map_mul {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) (a b : M) :
f (a * b) = (f a) * f b
@[protected]
f (a + b) = f a + f b
@[protected]
theorem monoid_hom.map_mul {M : Type u_1} {N : Type u_2} (f : M →* N) (a b : M) :
f (a * b) = (f a) * f b

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

@[protected]
theorem add_monoid_hom.map_add {M : Type u_1} {N : Type u_2} (f : M →+ N) (a b : M) :
f (a + b) = f a + f b

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

@[protected]
theorem monoid_with_zero_hom.map_mul {M : Type u_1} {N : Type u_2} (f : N) (a b : M) :
f (a * b) = (f a) * f b
theorem add_monoid_hom.map_add_eq_zero {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) {a b : M} (h : a + b = 0) :
f a + f b = 0
theorem monoid_hom.map_mul_eq_one {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {a b : M} (h : a * b = 1) :
(f a) * f b = 1
theorem monoid_hom.map_exists_right_inv {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {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 `is_unit.map`.

theorem add_monoid_hom.map_exists_right_neg {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) {x : M} (hx : ∃ (y : M), x + y = 0) :
∃ (y : N), f x + y = 0

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

theorem add_monoid_hom.map_exists_left_neg {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_zero_class N} (f : M →+ N) {x : M} (hx : ∃ (y : M), y + x = 0) :
∃ (y : N), y + f x = 0

Given an add_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 `is_add_unit.map`.

theorem monoid_hom.map_exists_left_inv {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : mul_one_class N} (f : M →* N) {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 `is_unit.map`.

G →+ G

Inversion on a commutative additive group, considered as an additive monoid homomorphism.

Equations
def comm_group.inv_monoid_hom {G : Type u_1} [comm_group G] :
G →* G

Inversion on a commutative group, considered as a monoid homomorphism.

Equations
def zero_hom.id (M : Type u_1) [has_zero M] :
M

The identity map from an type with zero to itself.

Equations
@[simp]
theorem one_hom.id_apply (M : Type u_1) [has_one M] (x : M) :
def one_hom.id (M : Type u_1) [has_one M] :
M

The identity map from a type with 1 to itself.

Equations
@[simp]
theorem zero_hom.id_apply (M : Type u_1) [has_zero M] (x : M) :
@[simp]
theorem mul_hom.id_apply (M : Type u_1) [has_mul M] (x : M) :
def mul_hom.id (M : Type u_1) [has_mul M] :
M

The identity map from a type with multiplication to itself.

Equations
@[simp]
theorem add_hom.id_apply (M : Type u_1) [has_add M] (x : M) :
M

The identity map from an type with addition to itself.

Equations
@[simp]
theorem monoid_hom.id_apply (M : Type u_1) (x : M) :
x = x
def monoid_hom.id (M : Type u_1)  :
M →* M

The identity map from a monoid to itself.

Equations
@[simp]
theorem add_monoid_hom.id_apply (M : Type u_1) (x : M) :
x = x
def add_monoid_hom.id (M : Type u_1)  :
M →+ M

The identity map from an additive monoid to itself.

Equations
def monoid_with_zero_hom.id (M : Type u_1)  :

The identity map from a monoid_with_zero to itself.

Equations
@[simp]
theorem monoid_with_zero_hom.id_apply (M : Type u_1) (x : M) :
= x
def zero_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (hnp : P) (hmn : N) :
P

Composition of `zero_hom`s as a `zero_hom`.

Equations
def one_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (hnp : P) (hmn : N) :
P

Composition of `one_hom`s as a `one_hom`.

Equations
def mul_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (hnp : P) (hmn : N) :
P

Composition of `mul_hom`s as a `mul_hom`.

Equations
def add_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (hnp : P) (hmn : N) :
P

Composition of `add_hom`s as a `add_hom`.

Equations
def monoid_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (hnp : N →* P) (hmn : M →* N) :
M →* P

Composition of monoid morphisms as a monoid morphism.

Equations
def add_monoid_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (hnp : N →+ P) (hmn : M →+ N) :
M →+ P

Equations
def monoid_with_zero_hom.comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (hnp : P) (hmn : N) :

Composition of `monoid_with_zero_hom`s as a `monoid_with_zero_hom`.

Equations
@[simp]
theorem zero_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (g : P) (f : N) :
(g.comp f) = g f
@[simp]
theorem one_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (g : P) (f : N) :
(g.comp f) = g f
@[simp]
theorem mul_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (g : P) (f : N) :
(g.comp f) = g f
@[simp]
theorem add_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : P) (f : N) :
(g.comp f) = g f
@[simp]
theorem add_monoid_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →+ P) (f : M →+ N) :
(g.comp f) = g f
@[simp]
theorem monoid_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →* P) (f : M →* N) :
(g.comp f) = g f
@[simp]
theorem monoid_with_zero_hom.coe_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : P) (f : N) :
(g.comp f) = g f
theorem one_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem zero_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem add_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem mul_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem monoid_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →* P) (f : M →* N) (x : M) :
(g.comp f) x = g (f x)
theorem add_monoid_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →+ P) (f : M →+ N) (x : M) :
(g.comp f) x = g (f x)
theorem monoid_with_zero_hom.comp_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem one_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_one M] [has_one N] [has_one P] [has_one Q] (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of monoid homomorphisms is associative.

theorem zero_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_zero M] [has_zero N] [has_zero P] [has_zero Q] (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem add_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_add M] [has_add N] [has_add P] [has_add Q] (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem mul_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_mul M] [has_mul N] [has_mul P] [has_mul Q] (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem add_monoid_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} (f : M →+ N) (g : N →+ P) (h : P →+ Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem monoid_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} (f : M →* N) (g : N →* P) (h : P →* Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem monoid_with_zero_hom.comp_assoc {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem zero_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] {g₁ g₂ : P} {f : N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem one_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] {g₁ g₂ : P} {f : N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem add_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] {g₁ g₂ : P} {f : N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem mul_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] {g₁ g₂ : P} {f : N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem add_monoid_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} {g₁ g₂ : N →+ P} {f : M →+ N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem monoid_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} {g₁ g₂ : N →* P} {f : M →* N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem monoid_with_zero_hom.cancel_right {M : Type u_1} {N : Type u_2} {P : Type u_3} {g₁ g₂ : P} {f : N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem one_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] {g : P} {f₁ f₂ : N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem zero_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] {g : P} {f₁ f₂ : N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem mul_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] {g : P} {f₁ f₂ : N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem add_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] {g : P} {f₁ f₂ : N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem monoid_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} {g : N →* P} {f₁ f₂ : M →* N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem add_monoid_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} {g : N →+ P} {f₁ f₂ : M →+ N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem monoid_with_zero_hom.cancel_left {M : Type u_1} {N : Type u_2} {P : Type u_3} {g : P} {f₁ f₂ : N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem add_monoid_hom.to_zero_hom_injective {M : Type u_1} {N : Type u_2}  :
theorem monoid_hom.to_one_hom_injective {M : Type u_1} {N : Type u_2}  :
theorem monoid_hom.to_mul_hom_injective {M : Type u_1} {N : Type u_2}  :
theorem monoid_with_zero_hom.to_monoid_hom_injective {M : Type u_1} {N : Type u_2}  :
theorem monoid_with_zero_hom.to_zero_hom_injective {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem zero_hom.comp_id {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.comp_id {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) :
f.comp (one_hom.id M) = f
@[simp]
theorem add_hom.comp_id {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
theorem mul_hom.comp_id {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) :
f.comp (mul_hom.id M) = f
@[simp]
theorem monoid_hom.comp_id {M : Type u_1} {N : Type u_2} (f : M →* N) :
f.comp = f
@[simp]
theorem add_monoid_hom.comp_id {M : Type u_1} {N : Type u_2} (f : M →+ N) :
f.comp = f
@[simp]
theorem monoid_with_zero_hom.comp_id {M : Type u_1} {N : Type u_2} (f : N) :
= f
@[simp]
theorem zero_hom.id_comp {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.id_comp {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (f : N) :
(one_hom.id N).comp f = f
@[simp]
theorem mul_hom.id_comp {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N) :
(mul_hom.id N).comp f = f
@[simp]
theorem add_hom.id_comp {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
theorem add_monoid_hom.id_comp {M : Type u_1} {N : Type u_2} (f : M →+ N) :
f = f
@[simp]
theorem monoid_hom.id_comp {M : Type u_1} {N : Type u_2} (f : M →* N) :
.comp f = f
@[simp]
theorem monoid_with_zero_hom.id_comp {M : Type u_1} {N : Type u_2} (f : N) :
= f
@[protected]
theorem monoid_hom.map_pow {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (a : M) (n : ) :
f (a ^ n) = f a ^ n
@[protected]
theorem add_monoid_hom.map_nsmul {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (a : M) (n : ) :
f (n a) = n f a
@[protected]
theorem add_monoid_hom.map_zsmul' {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x : M), f (-x) = -f x) (a : M) (n : ) :
f (n a) = n f a
@[protected]
theorem monoid_hom.map_zpow' {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹) (a : M) (n : ) :
f (a ^ n) = f a ^ n
theorem monoid_hom.map_div' {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹) (a b : M) :
f (a / b) = f a / f b
theorem add_monoid_hom.map_sub' {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x : M), f (-x) = -f x) (a b : M) :
f (a - b) = f a - f b
@[protected]
def monoid.End (M : Type u_1)  :
Type u_1

The monoid of endomorphisms.

Equations
@[protected, instance]
def monoid.End.monoid (M : Type u_1)  :
Equations
@[protected, instance]
def monoid.End.inhabited (M : Type u_1)  :
Equations
@[protected, instance]
def monoid.End.has_coe_to_fun (M : Type u_1)  :
(λ (_x : , M → M)
Equations
@[simp]
theorem monoid.coe_one (M : Type u_1)  :
@[simp]
theorem monoid.coe_mul (M : Type u_1) (f g : monoid.End M) :
f * g = f g
@[protected]
def add_monoid.End (A : Type u_7)  :
Type u_7

The monoid of endomorphisms.

Equations
@[protected, instance]
def add_monoid.End.monoid (A : Type u_7)  :
Equations
@[protected, instance]
def add_monoid.End.inhabited (A : Type u_7)  :
Equations
@[protected, instance]
def add_monoid.End.has_coe_to_fun (A : Type u_7)  :
(λ (_x : , A → A)
Equations
@[simp]
theorem add_monoid.coe_one (A : Type u_7)  :
@[simp]
theorem add_monoid.coe_mul (A : Type u_7) (f g : add_monoid.End A) :
f * g = f g
@[protected, instance]
def one_hom.has_one {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :

`1` is the homomorphism sending all elements to `1`.

Equations
@[protected, instance]
def zero_hom.has_zero {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :

`0` is the homomorphism sending all elements to `0`.

Equations
@[protected, instance]
def mul_hom.has_one {M : Type u_1} {N : Type u_2} [has_mul M]  :

`1` is the multiplicative homomorphism sending all elements to `1`.

Equations
@[protected, instance]
def add_hom.has_zero {M : Type u_1} {N : Type u_2} [has_add M]  :

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

Equations
@[protected, instance]
def monoid_hom.has_one {M : Type u_1} {N : Type u_2}  :

`1` is the monoid homomorphism sending all elements to `1`.

Equations
@[protected, instance]
def add_monoid_hom.has_zero {M : Type u_1} {N : Type u_2}  :

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

Equations
@[simp]
theorem one_hom.one_apply {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] (x : M) :
1 x = 1
@[simp]
theorem zero_hom.zero_apply {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] (x : M) :
0 x = 0
@[simp]
theorem add_monoid_hom.zero_apply {M : Type u_1} {N : Type u_2} (x : M) :
0 x = 0
@[simp]
theorem monoid_hom.one_apply {M : Type u_1} {N : Type u_2} (x : M) :
1 x = 1
@[simp]
theorem one_hom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (f : N) :
1.comp f = 1
@[simp]
theorem zero_hom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (f : N) :
0.comp f = 0
@[simp]
theorem one_hom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_one M] [has_one N] [has_one P] (f : P) :
f.comp 1 = 1
@[simp]
theorem zero_hom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_zero M] [has_zero N] [has_zero P] (f : P) :
f.comp 0 = 0
@[protected, instance]
def one_hom.inhabited {M : Type u_1} {N : Type u_2} [has_one M] [has_one N] :
Equations
@[protected, instance]
def zero_hom.inhabited {M : Type u_1} {N : Type u_2} [has_zero M] [has_zero N] :
Equations
@[protected, instance]
def add_hom.inhabited {M : Type u_1} {N : Type u_2} [has_add M]  :
Equations
@[protected, instance]
def mul_hom.inhabited {M : Type u_1} {N : Type u_2} [has_mul M]  :
Equations
@[protected, instance]
def add_monoid_hom.inhabited {M : Type u_1} {N : Type u_2}  :
Equations
@[protected, instance]
def monoid_hom.inhabited {M : Type u_1} {N : Type u_2}  :
Equations
@[protected, instance]
def monoid_with_zero_hom.inhabited {M : Type u_1}  :
Equations
@[protected, instance]
def monoid_hom.has_mul {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} [comm_monoid N] :

Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism sending `x` to `f x * g x`.

Equations
@[protected, instance]

Given two additive monoid morphisms `f`, `g` to an additive commutative monoid, `f + g` is the additive monoid morphism sending `x` to `f x + g x`.

Equations
@[simp]
theorem add_monoid_hom.add_apply {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} {mN : add_comm_monoid N} (f g : M →+ N) (x : M) :
(f + g) x = f x + g x
@[simp]
theorem monoid_hom.mul_apply {M : Type u_1} {N : Type u_2} {mM : mul_one_class M} {mN : comm_monoid N} (f g : M →* N) (x : M) :
(f * g) x = (f x) * g x
@[simp]
theorem monoid_hom.one_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : M →* N) :
1.comp f = 1
@[simp]
theorem add_monoid_hom.zero_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : M →+ N) :
0.comp f = 0
@[simp]
theorem monoid_hom.comp_one {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : N →* P) :
f.comp 1 = 1
@[simp]
theorem add_monoid_hom.comp_zero {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : N →+ P) :
f.comp 0 = 0
theorem add_monoid_hom.add_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} (g₁ g₂ : N →+ P) (f : M →+ N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem monoid_hom.mul_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [comm_monoid N] [comm_monoid P] (g₁ g₂ : N →* P) (f : M →* N) :
(g₁ * g₂).comp f = (g₁.comp f) * g₂.comp f
theorem add_monoid_hom.comp_add {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : N →+ P) (f₁ f₂ : M →+ N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
theorem monoid_hom.comp_mul {M : Type u_1} {N : Type u_2} {P : Type u_3} [comm_monoid N] [comm_monoid P] (g : N →* P) (f₁ f₂ : M →* N) :
g.comp (f₁ * f₂) = (g.comp f₁) * g.comp f₂
theorem add_monoid_hom.eq_on_neg {M : Type u_1} {G : Type u_2} [add_group G] [add_monoid M] {f g : G →+ M} {x : G} (h : f x = g x) :
f (-x) = g (-x)

If two homomorphism from an additive group to an additive monoid are equal at `x`, then they are equal at `-x`.

theorem monoid_hom.eq_on_inv {M : Type u_1} {G : Type u_2} [group G] [monoid M] {f g : G →* M} {x : G} (h : f x = g x) :

If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`.

@[protected]
theorem add_monoid_hom.map_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g : G) :
f (-g) = -f g
@[protected]
theorem monoid_hom.map_inv {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g : G) :

Group homomorphisms preserve inverse.

@[protected]
theorem add_monoid_hom.map_zsmul {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g : G) (n : ) :
f (n g) = n f g

Additive group homomorphisms preserve integer scaling.

@[protected]
theorem monoid_hom.map_zpow {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g : G) (n : ) :
f (g ^ n) = f g ^ n

Group homomorphisms preserve integer power.

@[protected]
theorem monoid_hom.map_div {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g h : G) :
f (g / h) = f g / f h

Group homomorphisms preserve division.

@[protected]
theorem add_monoid_hom.map_sub {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g h : G) :
f (g - h) = f g - f h

@[protected]
theorem add_monoid_hom.map_add_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (g h : G) :
f (g + -h) = f g + -f h
@[protected]
theorem monoid_hom.map_mul_inv {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (g h : G) :
f (g * h⁻¹) = (f g) * (f h)⁻¹

Group homomorphisms preserve division.

theorem monoid_hom.injective_iff {G : Type u_1} {H : Type u_2} [group G] (f : G →* H) :
∀ (a : G), f a = 1a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see `monoid_hom.injective_iff'`.

theorem add_monoid_hom.injective_iff {G : Type u_1} {H : Type u_2} [add_group G] (f : G →+ H) :
∀ (a : G), f a = 0a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial. For the iff statement on the triviality of the kernel, see `add_monoid_hom.injective_iff'`.

theorem add_monoid_hom.injective_iff' {G : Type u_1} {H : Type u_2} [add_group G] (f : G →+ H) :
∀ (a : G), f a = 0 a = 0

A homomorphism from an additive group to an additive monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see `add_monoid_hom.injective_iff`.

theorem monoid_hom.injective_iff' {G : Type u_1} {H : Type u_2} [group G] (f : G →* H) :
∀ (a : G), f a = 1 a = 1

A homomorphism from a group to a monoid is injective iff its kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see `monoid_hom.injective_iff`.

@[simp]
theorem monoid_hom.mk'_apply {M : Type u_1} {G : Type u_4} [mM : mul_one_class M] [group G] (f : M → G) (map_mul : ∀ (a b : M), f (a * b) = (f a) * f b) :
map_mul) = f
def add_monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : add_zero_class M] [add_group G] (f : M → G) (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
@[simp]
theorem add_monoid_hom.mk'_apply {M : Type u_1} {G : Type u_4} [mM : add_zero_class M] [add_group G] (f : M → G) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
map_mul) = f
def monoid_hom.mk' {M : Type u_1} {G : Type u_4} [mM : mul_one_class M] [group G] (f : M → G) (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
def add_monoid_hom.of_map_add_neg {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) :
G →+ H

Makes an additive group homomorphism from a proof that the map preserves the operation `λ a b, a + -b`. See also `add_monoid_hom.of_map_sub` for a version using `λ a b, a - b`.

Equations
• map_div =
def monoid_hom.of_map_mul_inv {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = (f a) * (f b)⁻¹) :
G →* H

Makes a group homomorphism from a proof that the map preserves right division `λ x y, x * y⁻¹`. See also `monoid_hom.of_map_div` for a version using `λ x y, x / y`.

Equations
• map_div =
@[simp]
theorem monoid_hom.coe_of_map_mul_inv {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (map_div : ∀ (a b : G), f (a * b⁻¹) = (f a) * (f b)⁻¹) :
map_div) = f
@[simp]
theorem add_monoid_hom.coe_of_map_add_neg {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) :
map_div) = f
def monoid_hom.of_map_div {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
G →* H

Define a morphism of additive groups given a map which respects ratios.

Equations
def add_monoid_hom.of_map_sub {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
G →+ H

Define a morphism of additive groups given a map which respects difference.

Equations
@[simp]
theorem monoid_hom.coe_of_map_div {G : Type u_4} [group G] {H : Type u_1} [group H] (f : G → H) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
hf) = f
@[simp]
theorem add_monoid_hom.coe_of_map_sub {G : Type u_4} [add_group G] {H : Type u_1} [add_group H] (f : G → H) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
= f
@[protected, instance]
def add_monoid_hom.has_neg {M : Type u_1} {G : Type u_2}  :

If `f` is an additive monoid homomorphism to an additive commutative group, then `-f` is the homomorphism sending `x` to `-(f x)`.

Equations
@[protected, instance]
def monoid_hom.has_inv {M : Type u_1} {G : Type u_2} [comm_group G] :

If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending `x` to `(f x)⁻¹`.

Equations
@[simp]
theorem monoid_hom.inv_apply {M : Type u_1} {G : Type u_2} {mM : mul_one_class M} {gG : comm_group G} (f : M →* G) (x : M) :
@[simp]
theorem add_monoid_hom.neg_apply {M : Type u_1} {G : Type u_2} {mM : add_zero_class M} {gG : add_comm_group G} (f : M →+ G) (x : M) :
(-f) x = -f x
@[simp]
theorem add_monoid_hom.neg_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} {mM : add_zero_class M} {gN : add_zero_class N} {gA : add_comm_group A} (φ : N →+ A) (ψ : M →+ N) :
(-φ).comp ψ = -φ.comp ψ
@[simp]
theorem monoid_hom.inv_comp {M : Type u_1} {N : Type u_2} {A : Type u_3} {mM : mul_one_class M} {gN : mul_one_class N} {gA : comm_group A} (φ : N →* A) (ψ : M →* N) :
φ⁻¹.comp ψ = (φ.comp ψ)⁻¹
@[simp]
theorem add_monoid_hom.comp_neg {M : Type u_1} {A : Type u_2} {B : Type u_3} {mM : add_zero_class M} {mA : add_comm_group A} {mB : add_comm_group B} (φ : A →+ B) (ψ : M →+ A) :
φ.comp (-ψ) = -φ.comp ψ
@[simp]
theorem monoid_hom.comp_inv {M : Type u_1} {A : Type u_2} {B : Type u_3} {mM : mul_one_class M} {mA : comm_group A} {mB : comm_group B} (φ : A →* B) (ψ : M →* A) :
φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹
@[protected, instance]
def add_monoid_hom.has_sub {M : Type u_1} {G : Type u_2}  :

If `f` and `g` are monoid homomorphisms to an additive commutative group, then `f - g` is the homomorphism sending `x` to `(f x) - (g x)`.

Equations
@[protected, instance]
def monoid_hom.has_div {M : Type u_1} {G : Type u_2} [comm_group G] :

If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism sending `x` to `(f x) / (g x)`.

Equations
@[simp]
theorem add_monoid_hom.sub_apply {M : Type u_1} {G : Type u_2} {mM : add_zero_class M} {gG : add_comm_group G} (f g : M →+ G) (x : M) :
(f - g) x = f x - g x
@[simp]
theorem monoid_hom.div_apply {M : Type u_1} {G : Type u_2} {mM : mul_one_class M} {gG : comm_group G} (f g : M →* G) (x : M) :
(f / g) x = f x / g x
@[protected, simp]
theorem add_semiconj_by.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] {a x y : M} [ N] (h : y) (f : F) :
add_semiconj_by (f a) (f x) (f y)
@[protected, simp]
theorem semiconj_by.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_mul M] [has_mul N] {a x y : M} [ N] (h : x y) (f : F) :
semiconj_by (f a) (f x) (f y)
@[protected, simp]
theorem add_commute.map {M : Type u_1} {N : Type u_2} {F : Type u_6} [has_add M] [has_add N] {x y : M} [ N] (h : y) (f : F) :