# mathlibdocumentation

algebra.hom.group

# 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 #

• `→+`: Bundled `add_monoid` homs. Also use for `add_group` homs.
• `→*`: Bundled `monoid` homs. Also use for `group` homs.
• `→*₀`: Bundled `monoid_with_zero` homs. Also use for `group_with_zero` 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 `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_9) (N : Type u_10) [has_zero M] [has_zero N] :
Type (max u_10 u_9)
• 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`.

Instances for `zero_hom`
@[instance]
def zero_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_zero M] [has_zero N] [self : N] :
M (λ (_x : M), N)
@[class]
structure zero_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_zero M] [has_zero N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `zero_hom_class`
• zero_hom_class.has_sizeof_inst
Type (max u_10 u_9)

`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`.

Instances for `add_hom`
@[class]
structure add_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_add M] [has_add N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `add_hom_class`
@[instance]
def add_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_add M] [has_add N] [self : N] :
M (λ (_x : M), N)
@[nolint]
def add_monoid_hom.to_add_hom {M : Type u_9} {N : Type u_10} (self : M →+ N) :
N
structure add_monoid_hom (M : Type u_9) (N : Type u_10)  :
Type (max u_10 u_9)

`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`.

Instances for `add_monoid_hom`
@[nolint]
def add_monoid_hom.to_zero_hom {M : Type u_9} {N : Type u_10} (self : M →+ N) :
N
@[class]
structure add_monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11))  :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `add_monoid_hom_class`
@[instance]
def add_monoid_hom_class.to_add_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
@[instance]
def add_monoid_hom_class.to_zero_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
structure one_hom (M : Type u_9) (N : Type u_10) [has_one M] [has_one N] :
Type (max u_10 u_9)
• 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`.

Instances for `one_hom`
@[class]
structure one_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_one M] [has_one N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `one_hom_class`
• one_hom_class.has_sizeof_inst
@[instance]
def one_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_one M] [has_one N] [self : N] :
M (λ (_x : M), N)
@[protected, instance]
def one_hom.one_hom_class {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] :
Equations
@[protected, instance]
def zero_hom.zero_hom_class {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] :
Equations
@[simp]
theorem map_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_one M] [has_one N] [ N] (f : F) :
f 1 = 1
@[simp]
theorem map_zero {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_zero M] [has_zero N] [ N] (f : F) :
f 0 = 0
theorem map_eq_one_iff {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [has_zero M] [has_zero N] [ N] (f : F) (hf : function.injective f) {x : M} :
f x = 0 x = 0
theorem map_ne_zero_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_zero R] [has_zero S] [ S] (f : F) (hf : function.injective f) {x : R} :
f x 0 x 0
theorem map_ne_one_iff {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_one R] [has_one S] [ S] (f : F) (hf : function.injective f) {x : R} :
f x 1 x 1
theorem ne_zero_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_zero R] [has_zero S] [ S] {f : F} {x : R} (hx : f x 0) :
x 0
theorem ne_one_of_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_one R] [has_one S] [ S] {f : F} {x : R} (hx : f x 1) :
x 1
@[protected, instance]
def zero_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_zero M] [has_zero N] [ N] :
(zero_hom M N)
Equations
@[protected, instance]
def one_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_one M] [has_one N] [ N] :
(one_hom M N)
Equations
structure mul_hom (M : Type u_9) (N : Type u_10) [has_mul M] [has_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 `non_unital_alg_hom` and `non_unital_ring_hom`, so a `mul_hom` is a non-unital monoid hom.

When possible, instead of parametrizing results over `(f : 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`.

Instances for `mul_hom`
@[instance]
def mul_hom_class.to_fun_like (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_mul M] [has_mul N] [self : N] :
M (λ (_x : M), N)
@[class]
structure mul_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [has_mul M] [has_mul N] :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `mul_hom_class`
• mul_hom_class.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
def mul_hom.mul_hom_class {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] :
Equations
@[simp]
theorem map_add {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [has_mul M] [has_mul N] [ N] (f : F) (x y : M) :
f (x * y) = f x * f y
@[protected, instance]
def mul_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_mul M] [has_mul N] [ N] :
(M →ₙ* N)
Equations
@[protected, instance]
def add_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_add M] [has_add N] [ N] :
Equations
structure monoid_hom (M : Type u_9) (N : Type u_10)  :
Type (max u_10 u_9)

`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`.

Instances for `monoid_hom`
@[nolint]
def monoid_hom.to_one_hom {M : Type u_9} {N : Type u_10} (self : M →* N) :
N
@[nolint]
def monoid_hom.to_mul_hom {M : Type u_9} {N : Type u_10} (self : M →* N) :
@[class]
structure monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11))  :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `monoid_hom_class`
• monoid_hom_class.has_sizeof_inst
@[instance]
def monoid_hom_class.to_one_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
@[instance]
def monoid_hom_class.to_mul_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
@[protected, instance]
Equations
@[protected, instance]
def monoid_hom.monoid_hom_class {M : Type u_3} {N : Type u_4}  :
Equations
@[protected, instance]
def add_monoid_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [ N] :
(M →+ N)
Equations
@[protected, instance]
def monoid_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [ N] :
(M →* N)
Equations
theorem map_mul_eq_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [ N] (f : F) {a b : M} (h : a * b = 1) :
f a * f b = 1
theorem map_add_eq_zero {M : Type u_3} {N : Type u_4} {F : Type u_8} [ N] (f : F) {a b : M} (h : a + b = 0) :
f a + f b = 0
theorem map_div' {G : Type u_6} {H : Type u_7} {F : Type u_8} [ H] (f : F) (hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹) (a b : G) :
f (a / b) = f a / f b
theorem map_sub' {G : Type u_6} {H : Type u_7} {F : Type u_8} [ H] (f : F) (hf : ∀ (a : G), f (-a) = -f a) (a b : G) :
f (a - b) = f a - f b
@[simp]
theorem map_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [ H] (f : F) (a : G) :

Group homomorphisms preserve inverse.

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

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

Group homomorphisms preserve division.

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

@[simp]
theorem map_div {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [ H] (f : F) (a 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} [add_group G] [ H] (f : F) (a b : G) :
f (a - b) = f a - f b

@[simp]
theorem map_pow {G : Type u_6} {H : Type u_7} {F : Type u_8} [monoid G] [monoid H] [ H] (f : F) (a : G) (n : ) :
f (a ^ n) = f a ^ n
theorem map_nsmul.aux {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_monoid G] [add_monoid H] [ H] (f : F) (a : G) (n : ) :
f (n a) = n f a
@[simp]
theorem map_nsmul {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_monoid G] [add_monoid H] [ H] (f : F) (n : ) (a : G) :
f (n a) = n f a
theorem map_zpow' {G : Type u_6} {H : Type u_7} {F : Type u_8} [ 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_6} {H : Type u_7} {F : Type u_8} [ H] (f : F) (hf : ∀ (x : G), f (-x) = -f x) (a : G) (n : ) :
f (n a) = n f a
@[simp]
theorem map_zpow {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [ H] (f : F) (g : G) (n : ) :
f (g ^ n) = f g ^ n

Group homomorphisms preserve integer power.

theorem map_zsmul.aux {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_group G] [ H] (f : F) (g : G) (n : ) :
f (n g) = n f g
theorem map_zsmul {G : Type u_6} {H : Type u_7} {F : Type u_8} [add_group G] [ H] (f : F) (n : ) (g : G) :
f (n g) = n f g

Additive group homomorphisms preserve integer scaling.

@[nolint]
def monoid_with_zero_hom.to_zero_hom {M : Type u_9} {N : Type u_10} (self : M →*₀ N) :
N
structure monoid_with_zero_hom (M : Type u_9) (N : Type u_10)  :
Type (max u_10 u_9)

`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`.

Instances for `monoid_with_zero_hom`
@[nolint]
def monoid_with_zero_hom.to_monoid_hom {M : Type u_9} {N : Type u_10} (self : M →*₀ N) :
M →* N
@[class]
structure monoid_with_zero_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11))  :
Type (max u_10 u_11 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 of this typeclass
Instances of other typeclasses for `monoid_with_zero_hom_class`
• monoid_with_zero_hom_class.has_sizeof_inst
@[instance]
def monoid_with_zero_hom_class.to_monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
@[instance]
def monoid_with_zero_hom_class.to_zero_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [self : N] :
N
@[protected, instance]
def monoid_with_zero_hom.monoid_with_zero_hom_class {M : Type u_3} {N : Type u_4}  :
M N
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [ N] :
(M →*₀ N)
Equations

Bundled morphisms can be down-cast to weaker bundlings

@[protected, instance]
def add_monoid_hom.has_coe_to_zero_hom {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {mM : mul_one_class M} {mN : mul_one_class N} :
has_coe (M →* N) (M →ₙ* N)
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_monoid_hom {M : Type u_3} {N : Type u_4} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
has_coe (M →*₀ N) (M →* N)
Equations
@[protected, instance]
def monoid_with_zero_hom.has_coe_to_zero_hom {M : Type u_3} {N : Type u_4} {mM : mul_zero_one_class M} {mN : mul_zero_one_class 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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : M →*₀ N) :
@[simp]
theorem monoid_with_zero_hom.coe_eq_to_zero_hom {M : Type u_3} {N : Type u_4} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} (f : M →*₀ N) :
@[protected, instance]
def zero_hom.has_coe_to_fun {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {mM : has_mul M} {mN : has_mul N} :
has_coe_to_fun (M →ₙ* N) (λ (_x : M →ₙ* N), M → N)
Equations
@[protected, instance]
def add_hom.has_coe_to_fun {M : Type u_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {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_3} {N : Type u_4} {mM : mul_zero_one_class M} {mN : mul_zero_one_class N} :
has_coe_to_fun (M →*₀ N) (λ (_x : M →*₀ N), M → N)
Equations
@[simp]
theorem zero_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : N) :
@[simp]
theorem add_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : N) :
@[simp]
theorem mul_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M →ₙ* N) :
@[simp]
theorem add_monoid_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
@[simp]
theorem one_hom.coe_mk {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} (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_3} {N : Type u_4} (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_3} {N : Type u_4} (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_3} {N : Type u_4} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_one_hom_coe {M : Type u_3} {N : Type u_4} (f : M →* N) :
@[simp]
theorem add_monoid_hom.to_add_hom_coe {M : Type u_3} {N : Type u_4} (f : M →+ N) :
@[simp]
theorem monoid_hom.to_mul_hom_coe {M : Type u_3} {N : Type u_4} (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_zero_hom_coe {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
@[simp]
theorem monoid_with_zero_hom.to_monoid_hom_coe {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
theorem zero_hom.ext {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem add_hom.ext {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} ⦃f g : M →* N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem add_monoid_hom.ext {M : Type u_3} {N : Type u_4} ⦃f g : M →+ N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_with_zero_hom.ext {M : Type u_3} {N : Type u_4} ⦃f g : M →*₀ N⦄ (h : ∀ (x : M), f x = g x) :
f = g
theorem zero_hom.congr_fun {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] {f g : N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem one_hom.congr_fun {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] {f g : N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem mul_hom.congr_fun {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M →ₙ* N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem add_hom.congr_fun {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f g : N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem monoid_hom.congr_fun {M : Type u_3} {N : Type u_4} {f g : M →* N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem add_monoid_hom.congr_fun {M : Type u_3} {N : Type u_4} {f g : M →+ N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem monoid_with_zero_hom.congr_fun {M : Type u_3} {N : Type u_4} {f g : M →*₀ N} (h : f = g) (x : M) :
f x = g x

Deprecated: use `fun_like.congr_fun` instead.

theorem one_hom.congr_arg {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem zero_hom.congr_arg {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem mul_hom.congr_arg {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M →ₙ* N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem add_hom.congr_arg {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem monoid_hom.congr_arg {M : Type u_3} {N : Type u_4} (f : M →* N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem add_monoid_hom.congr_arg {M : Type u_3} {N : Type u_4} (f : M →+ N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem monoid_with_zero_hom.congr_arg {M : Type u_3} {N : Type u_4} (f : M →*₀ N) {x y : M} (h : x = y) :
f x = f y

Deprecated: use `fun_like.congr_arg` instead.

theorem zero_hom.coe_inj {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] ⦃f g : N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem one_hom.coe_inj {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] ⦃f g : N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem add_hom.coe_inj {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] ⦃f g : N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem mul_hom.coe_inj {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] ⦃f g : M →ₙ* N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem add_monoid_hom.coe_inj {M : Type u_3} {N : Type u_4} ⦃f g : M →+ N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem monoid_hom.coe_inj {M : Type u_3} {N : Type u_4} ⦃f g : M →* N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem monoid_with_zero_hom.coe_inj {M : Type u_3} {N : Type u_4} ⦃f g : M →*₀ N⦄ (h : f = g) :
f = g

Deprecated: use `fun_like.coe_injective` instead.

theorem zero_hom.ext_iff {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] {f g : N} :
f = g ∀ (x : M), f x = g x

Deprecated: use `fun_like.ext_iff` instead.

theorem one_hom.ext_iff {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] {f g : N} :
f = g ∀ (x : M), f x = g x

Deprecated: use `fun_like.ext_iff` instead.

theorem add_hom.ext_iff {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M →ₙ* N} :
f = g ∀ (x : M), f x = g x

Deprecated: use `fun_like.ext_iff` instead.

theorem monoid_hom.ext_iff {M : Type u_3} {N : Type u_4} {f g : M →* N} :
f = g ∀ (x : M), f x = g x

Deprecated: use `fun_like.ext_iff` instead.

theorem add_monoid_hom.ext_iff {M : Type u_3} {N : Type u_4} {f g : M →+ N} :
f = g ∀ (x : M), f x = g x
theorem monoid_with_zero_hom.ext_iff {M : Type u_3} {N : Type u_4} {f g : M →*₀ N} :
f = g ∀ (x : M), f x = g x

Deprecated: use `fun_like.ext_iff` instead.

@[simp]
theorem zero_hom.mk_coe {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [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_monoid_hom.mk_coe {M : Type u_3} {N : Type u_4} (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_3} {N : Type u_4} (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_3} {N : Type u_4} (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
@[protected]
def zero_hom.copy {M : Type u_3} {N : Type u_4} {hM : has_zero M} {hN : has_zero N} (f : N) (f' : M → N) (h : f' = f) :
N

Copy of a `zero_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def one_hom.copy {M : Type u_3} {N : Type u_4} {hM : has_one M} {hN : has_one N} (f : N) (f' : M → N) (h : f' = f) :
N

Copy of a `one_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def add_hom.copy {M : Type u_3} {N : Type u_4} {hM : has_add M} {hN : has_add N} (f : N) (f' : M → N) (h : f' = f) :
N

Copy of an `add_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def mul_hom.copy {M : Type u_3} {N : Type u_4} {hM : has_mul M} {hN : has_mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = f) :

Copy of a `mul_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def add_monoid_hom.copy {M : Type u_3} {N : Type u_4} {hM : add_zero_class M} {hN : add_zero_class N} (f : M →+ N) (f' : M → N) (h : f' = f) :
M →+ N

Copy of an `add_monoid_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def monoid_hom.copy {M : Type u_3} {N : Type u_4} {hM : mul_one_class M} {hN : mul_one_class N} (f : M →* N) (f' : M → N) (h : f' = f) :
M →* N

Copy of a `monoid_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def monoid_with_zero_hom.copy {M : Type u_3} {N : Type u_4} {hM : mul_zero_one_class M} {hN : mul_zero_one_class N} (f : M →*₀ N) (f' : M → N) (h : f' = f) :
M →* N

Copy of a `monoid_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
theorem one_hom.map_one {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : N) :
f 1 = 1
@[protected]
theorem zero_hom.map_zero {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : N) :
f 0 = 0
@[protected]
theorem add_monoid_hom.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`.

@[protected]
theorem monoid_hom.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`.

@[protected]
theorem monoid_with_zero_hom.map_one {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
f 1 = 1
@[protected]
theorem monoid_with_zero_hom.map_zero {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
f 0 = 0
@[protected]
theorem mul_hom.map_mul {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M →ₙ* 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_3} {N : Type u_4} (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_3} {N : Type u_4} (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_3} {N : Type u_4} (f : M →*₀ N) (a b : M) :
f (a * b) = f a * f b
theorem monoid_hom.map_exists_right_inv {M : Type u_3} {N : Type u_4} {F : Type u_8} {mM : mul_one_class M} {mN : mul_one_class N} [ N] (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 `is_unit.map`.

theorem add_monoid_hom.map_exists_right_neg {M : Type u_3} {N : Type u_4} {F : Type u_8} {mM : add_zero_class M} {mN : add_zero_class N} [ N] (f : F) {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_3} {N : Type u_4} {F : Type u_8} {mM : add_zero_class M} {mN : add_zero_class N} [ N] (f : F) {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_3} {N : Type u_4} {F : Type u_8} {mM : mul_one_class M} {mN : mul_one_class N} [ N] (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 `is_unit.map`.

def neg_add_monoid_hom {α : Type u_1}  :
α →+ α

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

Equations
def inv_monoid_hom {α : Type u_1}  :
α →* α

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

Equations
@[simp]
theorem coe_inv_monoid_hom {α : Type u_1}  :
@[simp]
theorem inv_monoid_hom_apply {α : Type u_1} (a : α) :
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] :

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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) :

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

Equations
def add_hom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_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
def add_monoid_hom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (hnp : N →+ P) (hmn : M →+ N) :
M →+ P

Equations
def monoid_with_zero_hom.comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (hnp : N →*₀ P) (hmn : M →*₀ N) :

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

Equations
@[simp]
theorem zero_hom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
(g.comp f) = g f
@[simp]
theorem add_hom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} (g : N →+ P) (f : M →+ N) :
(g.comp f) = g f
@[simp]
theorem monoid_hom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (g : N →* P) (f : M →* N) :
(g.comp f) = g f
@[simp]
theorem monoid_with_zero_hom.coe_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (g : N →*₀ P) (f : M →*₀ N) :
(g.comp f) = g f
theorem one_hom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] (g : N →ₙ* P) (f : M →ₙ* N) (x : M) :
(g.comp f) x = g (f x)
theorem monoid_hom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} (g : N →* P) (f : M →* N) (x : M) :
(g.comp f) x = g (f x)
theorem add_monoid_hom.comp_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} (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_3} {N : Type u_4} {P : Type u_5} (g : N →*₀ P) (f : M →*₀ N) (x : M) :
(g.comp f) x = g (f x)
theorem one_hom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} [has_mul M] [has_mul N] [has_mul P] [has_mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem add_monoid_hom.comp_assoc {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} (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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} (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_3} {N : Type u_4} {P : Type u_5} {Q : Type u_1} (f : M →*₀ N) (g : N →*₀ P) (h : P →*₀ Q) :
(h.comp g).comp f = h.comp (g.comp f)
theorem zero_hom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] {g₁ g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem add_monoid_hom.cancel_right {M : Type u_3} {N : Type u_4} {P : Type u_5} {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_3} {N : Type u_4} {P : Type u_5} {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_3} {N : Type u_4} {P : Type u_5} {g₁ g₂ : N →*₀ P} {f : M →*₀ N} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem one_hom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] {g : N →ₙ* P} {f₁ f₂ : M →ₙ* N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem add_hom.cancel_left {M : Type u_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} {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_3} {N : Type u_4} {P : Type u_5} {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_3} {N : Type u_4} {P : Type u_5} {g : N →*₀ P} {f₁ f₂ : M →*₀ N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem add_monoid_hom.to_zero_hom_injective {M : Type u_3} {N : Type u_4}  :
theorem monoid_hom.to_one_hom_injective {M : Type u_3} {N : Type u_4}  :
theorem monoid_hom.to_mul_hom_injective {M : Type u_3} {N : Type u_4}  :
theorem monoid_with_zero_hom.to_monoid_hom_injective {M : Type u_3} {N : Type u_4}  :
theorem monoid_with_zero_hom.to_zero_hom_injective {M : Type u_3} {N : Type u_4}  :
@[simp]
theorem zero_hom.comp_id {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.comp_id {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : N) :
f.comp (one_hom.id M) = f
@[simp]
theorem add_hom.comp_id {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : N) :
@[simp]
theorem mul_hom.comp_id {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M →ₙ* N) :
f.comp (mul_hom.id M) = f
@[simp]
theorem monoid_hom.comp_id {M : Type u_3} {N : Type u_4} (f : M →* N) :
f.comp = f
@[simp]
theorem add_monoid_hom.comp_id {M : Type u_3} {N : Type u_4} (f : M →+ N) :
f.comp = f
@[simp]
theorem monoid_with_zero_hom.comp_id {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
= f
@[simp]
theorem zero_hom.id_comp {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : N) :
@[simp]
theorem one_hom.id_comp {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : N) :
(one_hom.id N).comp f = f
@[simp]
theorem mul_hom.id_comp {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M →ₙ* N) :
(mul_hom.id N).comp f = f
@[simp]
theorem add_hom.id_comp {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : N) :
@[simp]
theorem add_monoid_hom.id_comp {M : Type u_3} {N : Type u_4} (f : M →+ N) :
f = f
@[simp]
theorem monoid_hom.id_comp {M : Type u_3} {N : Type u_4} (f : M →* N) :
.comp f = f
@[simp]
theorem monoid_with_zero_hom.id_comp {M : Type u_3} {N : Type u_4} (f : M →*₀ N) :
= f
@[protected]
theorem monoid_hom.map_pow {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} (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_3} {N : Type u_4} (f : M →* N) (hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹) (a : M) (n : ) :
f (a ^ n) = f a ^ n
@[protected]
def monoid.End (M : Type u_3)  :
Type u_3

The monoid of endomorphisms.

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

The monoid of endomorphisms.

Equations
Instances for `add_monoid.End`
@[protected, instance]
def add_monoid.End.monoid (A : Type u_9)  :
Equations
@[protected, instance]
def add_monoid.End.inhabited (A : Type u_9)  :
Equations
@[protected, instance]
def add_monoid.End.has_coe_to_fun (A : Type u_9)  :
(λ (_x : , A → A)
Equations
@[simp]
theorem add_monoid.coe_one (A : Type u_9)  :
@[simp]
theorem add_monoid.coe_mul (A : Type u_9) (f g : add_monoid.End A) :
(f * g) = f g
@[protected, instance]
def one_hom.has_one {M : Type u_3} {N : Type u_4} [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_3} {N : Type u_4} [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_3} {N : Type u_4} [has_mul M]  :

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

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

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

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

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

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

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

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

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

Equations
@[protected, instance]
def mul_hom.has_mul {M : Type u_3} {N : Type u_4} [has_mul M]  :

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

Equations
@[simp]
theorem mul_hom.mul_apply {M : Type u_1} {N : Type u_2} {mM : has_mul M} {mN : comm_semigroup N} (f g : M →ₙ* N) (x : M) :
(f * g) x = f x * g x
@[simp]
theorem add_hom.add_apply {M : Type u_1} {N : Type u_2} {mM : has_add M} {mN : add_comm_semigroup N} (f g : N) (x : M) :
(f + g) x = f x + g x
theorem add_hom.add_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] [has_add N] (g₁ g₂ : P) (f : N) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem mul_hom.mul_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) :
(g₁ * g₂).comp f = g₁.comp f * g₂.comp f
theorem mul_hom.comp_mul {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
theorem add_hom.comp_add {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] (g : P) (f₁ f₂ : N) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
@[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_3} {N : Type u_4} {P : Type u_5} (f : M →* N) :
1.comp f = 1
@[simp]
theorem add_monoid_hom.zero_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (f : M →+ N) :
0.comp f = 0
@[simp]
theorem monoid_hom.comp_one {M : Type u_3} {N : Type u_4} {P : Type u_5} (f : N →* P) :
f.comp 1 = 1
@[simp]
theorem add_monoid_hom.comp_zero {M : Type u_3} {N : Type u_4} {P : Type u_5} (f : N →+ P) :
f.comp 0 = 0
theorem add_monoid_hom.add_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} (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_3} {N : Type u_4} {P : Type u_5} [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_3} {N : Type u_4} {P : Type u_5} (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_3} {N : Type u_4} {P : Type u_5} [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_3} {F : Type u_8} {G : Type u_1} [add_group G] [add_monoid M] [ M] {f g : F} {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_3} {F : Type u_8} {G : Type u_1} [group G] [monoid M] [ M] {f g : F} {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 {α : Type u_1} {β : Type u_2} [add_group α] (f : α →+ β) (a : α) :
f (-a) = -f a

@[protected]
theorem monoid_hom.map_inv {α : Type u_1} {β : Type u_2} [group α] (f : α →* β) (a : α) :

Group homomorphisms preserve inverse.

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

Additive group homomorphisms preserve integer scaling.

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

Group homomorphisms preserve integer power.

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

Group homomorphisms preserve division.

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

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

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

Group homomorphisms preserve division.

theorem injective_iff_map_eq_one {F : Type u_8} {G : Type u_1} {H : Type u_2} [group G] [ H] (f : F) :
∀ (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 `injective_iff_map_eq_one'`.

theorem injective_iff_map_eq_zero {F : Type u_8} {G : Type u_1} {H : Type u_2} [add_group G] [ H] (f : F) :
∀ (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 `injective_iff_map_eq_zero'`.

theorem injective_iff_map_eq_zero' {F : Type u_8} {G : Type u_1} {H : Type u_2} [add_group G] [ H] (f : F) :
∀ (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 `injective_iff_map_eq_zero`.

theorem injective_iff_map_eq_one' {F : Type u_8} {G : Type u_1} {H : Type u_2} [group G] [ H] (f : F) :
∀ (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 `injective_iff_map_eq_one`.

@[simp]
theorem monoid_hom.mk'_apply {M : Type u_3} {G : Type u_6} [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_3} {G : Type u_6} [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_3} {G : Type u_6} [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_3} {G : Type u_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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, instance]
def monoid_with_zero_hom.has_mul {M : Type u_1} {N : Type u_2} {hM : mul_zero_one_class M}  :

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

Equations
@[protected, simp]
theorem add_semiconj_by.map {M : Type u_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [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_3} {N : Type u_4} {F : Type u_8} [has_add M] [has_add N] {x y : M} [ N] (h : y) (f : F) :