mathlib documentation

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:

Notations #

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 #

monoid_hom, add_monoid_hom

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 : zero_hom_class F M N] :
fun_like F 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)

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
structure add_hom (M : Type u_9) (N : Type u_10) [has_add M] [has_add N] :
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)

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
  • add_hom_class.has_sizeof_inst
@[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 : add_hom_class F M N] :
fun_like F M (λ (_x : M), N)
@[nolint]
def add_monoid_hom.to_add_hom {M : Type u_9} {N : Type u_10} [add_zero_class M] [add_zero_class N] (self : M →+ N) :
structure add_monoid_hom (M : Type u_9) (N : Type u_10) [add_zero_class M] [add_zero_class N] :
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} [add_zero_class M] [add_zero_class N] (self : M →+ N) :
@[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)) [add_zero_class M] [add_zero_class N] [self : add_monoid_hom_class F M 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)) [add_zero_class M] [add_zero_class N] [self : add_monoid_hom_class F M 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)

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 : one_hom_class F M N] :
fun_like F 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] [one_hom_class F M 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] [zero_hom_class F M 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] [one_hom_class F M 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] [zero_hom_class F M 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] [zero_hom_class F R 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] [one_hom_class F R 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] [zero_hom_class F R 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] [one_hom_class F R 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] [zero_hom_class F 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] [one_hom_class F 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 : mul_hom_class F M N] :
fun_like F 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)

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]
def add_hom.add_hom_class {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] :
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] [add_hom_class F M 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] [mul_hom_class F M 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] [mul_hom_class F 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] [add_hom_class F M N] :
Equations
structure monoid_hom (M : Type u_9) (N : Type u_10) [mul_one_class M] [mul_one_class N] :
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} [mul_one_class M] [mul_one_class N] (self : M →* N) :
@[nolint]
def monoid_hom.to_mul_hom {M : Type u_9} {N : Type u_10} [mul_one_class M] [mul_one_class N] (self : M →* N) :
@[class]
structure monoid_hom_class (F : Type u_9) (M : out_param (Type u_10)) (N : out_param (Type u_11)) [mul_one_class M] [mul_one_class N] :
Type (max u_10 u_11 u_9)

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)) [mul_one_class M] [mul_one_class N] [self : monoid_hom_class F M 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)) [mul_one_class M] [mul_one_class N] [self : monoid_hom_class F M N] :
@[protected, instance]
def add_monoid_hom.add_monoid_hom_class {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] :
Equations
@[protected, instance]
def monoid_hom.monoid_hom_class {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] :
Equations
@[protected, instance]
def add_monoid_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class F M N] :
has_coe_t F (M →+ N)
Equations
@[protected, instance]
def monoid_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M N] :
has_coe_t F (M →* N)
Equations
theorem map_mul_eq_one {M : Type u_3} {N : Type u_4} {F : Type u_8} [mul_one_class M] [mul_one_class N] [monoid_hom_class F M 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} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class F M 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} [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G 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} [sub_neg_monoid G] [sub_neg_monoid H] [add_monoid_hom_class F G 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] [division_monoid H] [monoid_hom_class F 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] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F) (a : G) :
f (-a) = -f a

Additive group homomorphisms preserve negation.

@[simp]
theorem map_mul_inv {G : Type u_6} {H : Type u_7} {F : Type u_8} [group G] [division_monoid H] [monoid_hom_class F 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] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F) (a b : G) :
f (a + -b) = f a + -f b

Additive group homomorphisms preserve subtraction.

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

Additive group homomorphisms preserve subtraction.

@[simp]
theorem map_pow {G : Type u_6} {H : Type u_7} {F : Type u_8} [monoid G] [monoid H] [monoid_hom_class F G 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] [add_monoid_hom_class F G 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] [add_monoid_hom_class F G 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} [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G 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} [sub_neg_monoid G] [sub_neg_monoid H] [add_monoid_hom_class F G 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] [division_monoid H] [monoid_hom_class F 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] [subtraction_monoid H] [add_monoid_hom_class F 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] [subtraction_monoid H] [add_monoid_hom_class F 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} [mul_zero_one_class M] [mul_zero_one_class N] (self : M →*₀ N) :
structure monoid_with_zero_hom (M : Type u_9) (N : Type u_10) [mul_zero_one_class M] [mul_zero_one_class N] :
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} [mul_zero_one_class M] [mul_zero_one_class N] (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)) [mul_zero_one_class M] [mul_zero_one_class N] :
Type (max u_10 u_11 u_9)

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)) [mul_zero_one_class M] [mul_zero_one_class N] [self : monoid_with_zero_hom_class F M 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)) [mul_zero_one_class M] [mul_zero_one_class N] [self : monoid_with_zero_hom_class F M N] :
@[protected, instance]
def monoid_with_zero_hom.has_coe_t {M : Type u_3} {N : Type u_4} {F : Type u_8} [mul_zero_one_class M] [mul_zero_one_class N] [monoid_with_zero_hom_class F 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]
def add_monoid_hom.has_coe_to_add_hom {M : Type u_3} {N : Type u_4} {mM : add_zero_class M} {mN : add_zero_class N} :
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

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 : zero_hom M 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 : one_hom M 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 : add_hom M 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 : zero_hom M N) :
@[simp]
theorem one_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : one_hom M N) :
@[simp]
theorem add_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : add_hom M 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} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (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} [add_zero_class M] [add_zero_class N] (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} [mul_one_class M] [mul_one_class N] (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} [mul_zero_one_class M] [mul_zero_one_class N] (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} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_one_hom_coe {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem add_monoid_hom.to_add_hom_coe {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.to_mul_hom_coe {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.to_zero_hom_coe {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
@[simp]
theorem monoid_with_zero_hom.to_monoid_hom_coe {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
theorem zero_hom.ext {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] ⦃f g : zero_hom M 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 : one_hom M 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 : add_hom M N⦄ (h : ∀ (x : M), f x = g x) :
f = g
@[ext]
theorem monoid_hom.ext {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] ⦃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} [add_zero_class M] [add_zero_class N] ⦃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} [mul_zero_one_class M] [mul_zero_one_class N] ⦃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 : zero_hom M 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 : one_hom M 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 : add_hom M 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} [mul_one_class M] [mul_one_class N] {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} [add_zero_class M] [add_zero_class N] {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} [mul_zero_one_class M] [mul_zero_one_class N] {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 : one_hom M 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 : zero_hom M 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 : add_hom M 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} [mul_one_class M] [mul_one_class N] (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} [add_zero_class M] [add_zero_class N] (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} [mul_zero_one_class M] [mul_zero_one_class N] (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 : zero_hom M 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 : one_hom M 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 : add_hom M 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} [add_zero_class M] [add_zero_class N] ⦃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} [mul_one_class M] [mul_one_class N] ⦃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} [mul_zero_one_class M] [mul_zero_one_class N] ⦃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 : zero_hom M 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 : one_hom M 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 : add_hom M 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} [mul_one_class M] [mul_one_class N] {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} [add_zero_class M] [add_zero_class N] {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} [mul_zero_one_class M] [mul_zero_one_class N] {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 : zero_hom M 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 : one_hom M 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 : add_hom M 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} [add_zero_class M] [add_zero_class N] (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} [mul_one_class M] [mul_one_class N] (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} [mul_zero_one_class M] [mul_zero_one_class N] (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 : zero_hom M N) (f' : M → N) (h : f' = f) :

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 : one_hom M N) (f' : M → N) (h : f' = f) :

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 : add_hom M N) (f' : M → N) (h : f' = f) :

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 : one_hom M 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 : zero_hom M N) :
f 0 = 0
@[protected]
theorem add_monoid_hom.map_zero {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] (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} [mul_one_class M] [mul_one_class N] (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} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
f 1 = 1
@[protected]
theorem monoid_with_zero_hom.map_zero {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (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]
theorem add_hom.map_add {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : add_hom M N) (a b : M) :
f (a + b) = f a + f b
@[protected]
theorem monoid_hom.map_mul {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (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} [add_zero_class M] [add_zero_class N] (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} [mul_zero_one_class M] [mul_zero_one_class N] (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} [monoid_hom_class F M 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} [add_monoid_hom_class F M 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} [add_monoid_hom_class F M 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} [monoid_hom_class F M 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} [subtraction_comm_monoid α] :
α →+ α

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

Equations
def inv_monoid_hom {α : Type u_1} [division_comm_monoid α] :
α →* α

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

Equations
@[simp]
theorem inv_monoid_hom_apply {α : Type u_1} [division_comm_monoid α] (a : α) :
def zero_hom.id (M : Type u_1) [has_zero 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] :

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) :
def add_hom.id (M : Type u_1) [has_add M] :

The identity map from an type with addition to itself.

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

The identity map from a monoid to itself.

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

The identity map from an additive monoid to itself.

Equations
def monoid_with_zero_hom.id (M : Type u_1) [mul_zero_one_class M] :

The identity map from a monoid_with_zero to itself.

Equations
@[simp]
theorem monoid_with_zero_hom.id_apply (M : Type u_1) [mul_zero_one_class M] (x : M) :
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 : zero_hom N P) (hmn : zero_hom M N) :

Composition of zero_homs 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 : one_hom N P) (hmn : one_hom M N) :

Composition of one_homs 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_homs 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 : add_hom N P) (hmn : add_hom M N) :

Composition of add_homs as a add_hom.

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

Composition of additive monoid morphisms as an additive monoid morphism.

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

Composition of monoid_with_zero_homs 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 : zero_hom N P) (f : zero_hom M 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 : one_hom N P) (f : one_hom M 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 : add_hom N P) (f : add_hom M 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} [add_zero_class M] [add_zero_class N] [add_zero_class P] (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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (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} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] (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 : one_hom N P) (f : one_hom M 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 : zero_hom N P) (f : zero_hom M 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 : add_hom N P) (f : add_hom M 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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (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} [add_zero_class M] [add_zero_class N] [add_zero_class P] (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} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] (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 : one_hom M N) (g : one_hom N P) (h : one_hom P 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 : zero_hom M N) (g : zero_hom N P) (h : zero_hom P 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 : add_hom M N) (g : add_hom N P) (h : add_hom P 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} [add_zero_class M] [add_zero_class N] [add_zero_class P] [add_zero_class Q] (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} [mul_one_class M] [mul_one_class N] [mul_one_class P] [mul_one_class Q] (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} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] [mul_zero_one_class Q] (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₂ : zero_hom N P} {f : zero_hom M 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₂ : one_hom N P} {f : one_hom M 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₂ : add_hom N P} {f : add_hom M 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} [add_zero_class M] [add_zero_class N] [add_zero_class P] {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} [mul_one_class M] [mul_one_class N] [mul_one_class P] {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} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] {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 : one_hom N P} {f₁ f₂ : one_hom M 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 : zero_hom N P} {f₁ f₂ : zero_hom M 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 : add_hom N P} {f₁ f₂ : add_hom M 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} [mul_one_class M] [mul_one_class N] [mul_one_class P] {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} [add_zero_class M] [add_zero_class N] [add_zero_class P] {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} [mul_zero_one_class M] [mul_zero_one_class N] [mul_zero_one_class P] {g : N →*₀ P} {f₁ f₂ : M →*₀ N} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[simp]
theorem zero_hom.comp_id {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : zero_hom M N) :
@[simp]
theorem one_hom.comp_id {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : one_hom M 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 : add_hom M N) :
f.comp (add_hom.id M) = f
@[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} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem add_monoid_hom.comp_id {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_with_zero_hom.comp_id {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
@[simp]
theorem zero_hom.id_comp {M : Type u_3} {N : Type u_4} [has_zero M] [has_zero N] (f : zero_hom M N) :
@[simp]
theorem one_hom.id_comp {M : Type u_3} {N : Type u_4} [has_one M] [has_one N] (f : one_hom M 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 : add_hom M N) :
(add_hom.id N).comp f = f
@[simp]
theorem add_monoid_hom.id_comp {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
@[simp]
theorem monoid_hom.id_comp {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (f : M →* N) :
@[simp]
theorem monoid_with_zero_hom.id_comp {M : Type u_3} {N : Type u_4} [mul_zero_one_class M] [mul_zero_one_class N] (f : M →*₀ N) :
@[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} [sub_neg_monoid M] [sub_neg_monoid N] (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} [div_inv_monoid M] [div_inv_monoid N] (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) [mul_one_class M] :
Type u_3

The monoid of endomorphisms.

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

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] [add_zero_class N] :

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} [mul_one_class M] [mul_one_class N] :

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} [add_zero_class M] [add_zero_class N] :

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} [add_zero_class M] [add_zero_class N] (x : M) :
0 x = 0
@[simp]
theorem monoid_hom.one_apply {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (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 : one_hom M 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 : zero_hom M 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 : one_hom N 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 : zero_hom N 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] [add_zero_class N] :
Equations
@[protected, instance]
def mul_hom.inhabited {M : Type u_3} {N : Type u_4} [has_mul M] [mul_one_class N] :
Equations
@[protected, instance]
def add_monoid_hom.inhabited {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class N] :
Equations
@[protected, instance]
def monoid_hom.inhabited {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_hom.has_add {M : Type u_3} {N : Type u_4} [has_add M] [add_comm_semigroup N] :

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] [comm_semigroup N] :

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 : add_hom M 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] [add_comm_semigroup P] (g₁ g₂ : add_hom N P) (f : add_hom M 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] [comm_semigroup P] (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] [comm_semigroup N] [comm_semigroup P] (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] [add_comm_semigroup N] [add_comm_semigroup P] (g : add_hom N P) (f₁ f₂ : add_hom M 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]
def add_monoid_hom.has_add {M : Type u_1} {N : Type u_2} {mM : add_zero_class M} [add_comm_monoid N] :

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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (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} [add_zero_class M] [add_zero_class N] [add_zero_class P] (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} [mul_one_class M] [mul_one_class N] [mul_one_class P] (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} [add_zero_class M] [add_zero_class N] [add_zero_class P] (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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (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} [mul_one_class M] [mul_one_class 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_3} {N : Type u_4} {P : Type u_5} [add_zero_class M] [add_comm_monoid N] [add_comm_monoid P] (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} [mul_one_class M] [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] [add_monoid_hom_class F G 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] [monoid_hom_class F G 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 α] [subtraction_monoid β] (f : α →+ β) (a : α) :
f (-a) = -f a

Additive group homomorphisms preserve negation.

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

Group homomorphisms preserve inverse.

@[protected]
theorem add_monoid_hom.map_zsmul {α : Type u_1} {β : Type u_2} [add_group α] [subtraction_monoid β] (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 α] [division_monoid β] (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 α] [division_monoid β] (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 α] [subtraction_monoid β] (f : α →+ β) (g h : α) :
f (g - h) = f g - f h

Additive group homomorphisms preserve subtraction.

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

Additive group homomorphisms preserve subtraction.

@[protected]
theorem monoid_hom.map_mul_inv {α : Type u_1} {β : Type u_2} [group α] [division_monoid β] (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] [mul_one_class H] [monoid_hom_class F G H] (f : F) :
function.injective 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] [add_zero_class H] [add_monoid_hom_class F G H] (f : F) :
function.injective 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] [add_zero_class H] [add_monoid_hom_class F G H] (f : F) :
function.injective 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] [mul_one_class H] [monoid_hom_class F G H] (f : F) :
function.injective 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) :
(monoid_hom.mk' f 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) :
(add_monoid_hom.mk' f 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
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
@[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)⁻¹) :
@[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) :
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) :
@[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) :
@[protected, instance]
def add_monoid_hom.has_neg {M : Type u_1} {G : Type u_2} [add_zero_class M] [add_comm_group G] :

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} [mul_one_class M] [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} [add_zero_class M] [add_comm_group G] :

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} [mul_one_class M] [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} [comm_monoid_with_zero N] :

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} [add_hom_class F M N] (h : add_semiconj_by a x 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} [mul_hom_class F M N] (h : semiconj_by a 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} [add_hom_class F M N] (h : add_commute x y) (f : F) :
add_commute (f x) (f y)
@[protected, simp]
theorem commute.map {M : Type u_3} {N : Type u_4} {F : Type u_8} [has_mul M] [has_mul N] {x y : M} [mul_hom_class F M N] (h : commute x y) (f : F) :
commute (f x) (f y)