# Documentation

Mathlib.Algebra.Hom.Group.Basic

theorem NeZero.of_map {F : Type u_8} {R : Type u_9} {M : Type u_10} [Zero R] [Zero M] [ZeroHomClass F R M] (f : F) {r : R} [neZero : NeZero (f r)] :
theorem NeZero.of_injective {F : Type u_8} {R : Type u_9} {M : Type u_10} [Zero R] {r : R} [] [Zero M] [ZeroHomClass F R M] {f : F} (hf : ) :
NeZero (f r)
theorem negAddMonoidHom.proof_1 {α : Type u_1} :
-0 = 0
def negAddMonoidHom {α : Type u_1} :
α →+ α

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

Instances For
def invMonoidHom {α : Type u_1} :
α →* α

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

Instances For
@[simp]
theorem coe_invMonoidHom {α : Type u_1} :
invMonoidHom = Inv.inv
@[simp]
theorem invMonoidHom_apply {α : Type u_1} (a : α) :
invMonoidHom a = a⁻¹

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

f (x + y) + g (x + y) = f x + g x + (f y + g y)
instance MulHom.instMulMulHomToMulToSemigroup {M : Type u_3} {N : Type u_4} [Mul M] [] :
Mul (M →ₙ* N)

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

@[simp]
↑(f + g) x = f x + g x
@[simp]
theorem MulHom.mul_apply {M : Type u_9} {N : Type u_10} [Mul M] [] (f : M →ₙ* N) (g : M →ₙ* N) (x : M) :
↑(f * g) x = f x * g x
theorem MulHom.mul_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [] (g₁ : N →ₙ* P) (g₂ : N →ₙ* P) (f : M →ₙ* N) :
MulHom.comp (g₁ * g₂) f = MulHom.comp g₁ f * MulHom.comp g₂ f
theorem AddHom.comp_add {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [] [] (g : AddHom N P) (f₁ : AddHom M N) (f₂ : AddHom M N) :
theorem MulHom.comp_mul {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [] [] (g : N →ₙ* P) (f₁ : M →ₙ* N) (f₂ : M →ₙ* N) :
MulHom.comp g (f₁ * f₂) = MulHom.comp g f₁ * MulHom.comp g f₂
theorem AddMonoidHom.add.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M →+ N) (x : M) (y : M) :
f (x + y) + g (x + y) = f x + g x + (f y + g y)
instance AddMonoidHom.add {M : Type u_9} {N : Type u_10} [] [] :

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.

theorem AddMonoidHom.add.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M →+ N) :
f 0 + g 0 = 0
instance MonoidHom.mul {M : Type u_9} {N : Type u_10} [] [] :
Mul (M →* N)

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

@[simp]
theorem AddMonoidHom.add_apply {M : Type u_9} {N : Type u_10} [] [] (f : M →+ N) (g : M →+ N) (x : M) :
↑(f + g) x = f x + g x
@[simp]
theorem MonoidHom.mul_apply {M : Type u_9} {N : Type u_10} [] [] (f : M →* N) (g : M →* N) (x : M) :
↑(f * g) x = f x * g x
theorem AddMonoidHom.add_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g₁ : N →+ P) (g₂ : N →+ P) (f : M →+ N) :
AddMonoidHom.comp (g₁ + g₂) f = +
theorem MonoidHom.mul_comp {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g₁ : N →* P) (g₂ : N →* P) (f : M →* N) :
MonoidHom.comp (g₁ * g₂) f = *
theorem AddMonoidHom.comp_add {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →+ P) (f₁ : M →+ N) (f₂ : M →+ N) :
AddMonoidHom.comp g (f₁ + f₂) = +
theorem MonoidHom.comp_mul {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (g : N →* P) (f₁ : M →* N) (f₂ : M →* N) :
MonoidHom.comp g (f₁ * f₂) = *
theorem injective_iff_map_eq_zero {F : Type u_8} {G : Type u_9} {H : Type u_10} [] [] [] (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_one {F : Type u_8} {G : Type u_9} {H : Type u_10} [] [] [] (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_9} {H : Type u_10} [] [] [] (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_9} {H : Type u_10} [] [] [] (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.

def AddMonoidHom.ofMapAddNeg {G : Type u_6} [] {H : Type u_9} [] (f : GH) (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 fun a b => a + -b. See also AddMonoidHom.ofMapSub for a version using fun a b => a - b.

Instances For
theorem AddMonoidHom.ofMapAddNeg.proof_1 {G : Type u_2} [] {H : Type u_1} [] (f : GH) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) (x : G) (y : G) :
f (x + y) = f x + f y
def MonoidHom.ofMapMulInv {G : Type u_6} [] {H : Type u_9} [] (f : GH) (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 fun x y => x * y⁻¹. See also MonoidHom.of_map_div for a version using fun x y => x / y.

Instances For
@[simp]
theorem AddMonoidHom.coe_of_map_add_neg {G : Type u_6} [] {H : Type u_9} [] (f : GH) (map_div : ∀ (a b : G), f (a + -b) = f a + -f b) :
@[simp]
theorem MonoidHom.coe_of_map_mul_inv {G : Type u_6} [] {H : Type u_9} [] (f : GH) (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹) :
↑(MonoidHom.ofMapMulInv f map_div) = f
def AddMonoidHom.ofMapSub {G : Type u_6} [] {H : Type u_9} [] (f : GH) (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.

Instances For
theorem AddMonoidHom.ofMapSub.proof_1 {G : Type u_2} [] {H : Type u_1} [] (f : GH) (hf : ∀ (x y : G), f (x - y) = f x - f y) (a : G) (a : G) :
f (a + -a) = f a + -f a
def MonoidHom.ofMapDiv {G : Type u_6} [] {H : Type u_9} [] (f : GH) (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.

Instances For
@[simp]
theorem AddMonoidHom.coe_of_map_sub {G : Type u_6} [] {H : Type u_9} [] (f : GH) (hf : ∀ (x y : G), f (x - y) = f x - f y) :
↑() = f
@[simp]
theorem MonoidHom.coe_of_map_div {G : Type u_6} [] {H : Type u_9} [] (f : GH) (hf : ∀ (x y : G), f (x / y) = f x / f y) :
↑() = f
-f (a + b) = -f a + -f b

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

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

@[simp]
theorem AddMonoidHom.neg_apply {M : Type u_9} {G : Type u_10} [] [] (f : M →+ G) (x : M) :
↑(-f) x = -f x
@[simp]
theorem MonoidHom.inv_apply {M : Type u_9} {G : Type u_10} [] [] (f : M →* G) (x : M) :
f⁻¹ x = (f x)⁻¹
@[simp]
theorem AddMonoidHom.neg_comp {M : Type u_9} {N : Type u_10} {A : Type u_11} [] [] [] (φ : N →+ A) (ψ : M →+ N) :
=
@[simp]
theorem MonoidHom.inv_comp {M : Type u_9} {N : Type u_10} {A : Type u_11} [] [] [] (φ : N →* A) (ψ : M →* N) :
= ()⁻¹
@[simp]
theorem AddMonoidHom.comp_neg {M : Type u_9} {A : Type u_10} {B : Type u_11} [] [] [] (φ : A →+ B) (ψ : M →+ A) :
=
@[simp]
theorem MonoidHom.comp_inv {M : Type u_9} {A : Type u_10} {B : Type u_11} [] [] [] (φ : A →* B) (ψ : M →* A) :
= ()⁻¹

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

If f and g are monoid homomorphisms to a commutative group, then f / g is the homomorphism sending x to (f x) / (g x).
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.