# Instances on spaces of monoid and group morphisms #

This file does two things involving AddMonoid.End and Ring. They are separate, and if someone would like to split this file in two that may be helpful.

• We provide the Ring structure on AddMonoid.End.
• Results about AddMonoid.End R when R is a ring.
Equations
@[simp]
theorem AddMonoid.End.natCast_apply {M : Type uM} [] (n : ) (m : M) :
n m = n m

See also AddMonoid.End.natCast_def.

@[simp]
theorem AddMonoid.End.ofNat_apply {M : Type uM} [] (n : ) [n.AtLeastTwo] (m : M) :
() m = n m
instance AddMonoid.End.instSemiring {M : Type uM} [] :
Equations
• One or more equations did not get rendered due to their size.
instance AddMonoid.End.instRing {M : Type uM} [] :
Equations

### Miscellaneous definitions #

This file used to import Algebra.GroupPower.Basic, hence it was not possible to import it in some of the lower-level files like Algebra.Ring.Basic. The following lemmas should be rehomed now that Algebra.GroupPower.Basic was deleted.

def AddMonoidHom.mul {R : Type u_1} :
R →+ R →+ R

Multiplication of an element of a (semi)ring is an AddMonoidHom in both arguments.

This is a more-strongly bundled version of AddMonoidHom.mulLeft and AddMonoidHom.mulRight.

Stronger versions of this exists for algebras as LinearMap.mul, NonUnitalAlgHom.mul and Algebra.lmul.

Equations
Instances For
theorem AddMonoidHom.mul_apply {R : Type u_1} (x : R) (y : R) :
(AddMonoidHom.mul x) y = x * y
@[simp]
theorem AddMonoidHom.coe_mul {R : Type u_1} :
@[simp]
theorem AddMonoidHom.coe_flip_mul {R : Type u_1} :
theorem AddMonoidHom.map_mul_iff {R : Type u_1} {S : Type u_2} (f : R →+ S) :
(∀ (x y : R), f (x * y) = f x * f y) AddMonoidHom.mul.compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f

An AddMonoidHom preserves multiplication if pre- and post- composition with AddMonoidHom.mul are equivalent. By converting the statement into an equality of AddMonoidHoms, this lemma allows various specialized ext lemmas about →+ to then be applied.

theorem AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {R : Type u_1} {a : R} :
∀ (b : R), Commute a b
theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {R : Type u_1} {b : R} :
∀ (a : R), Commute a b
@[simp]
theorem AddMonoid.End.mulLeft_apply_apply {R : Type u_1} (r : R) :
∀ (x : R), (AddMonoid.End.mulLeft r) x = r * x
def AddMonoid.End.mulLeft {R : Type u_1} :

The left multiplication map: (a, b) ↦ a * b. See also AddMonoidHom.mulLeft.

Equations
The right multiplication map: (a, b) ↦ b * a. See also AddMonoidHom.mulRight.