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

source
instance AddMonoid.End.instAddMonoidWithOne (M : Type u_1) [AddCommMonoid M] :
AddMonoidWithOne (AddMonoid.End M)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem AddMonoid.End.natCast_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) (m : M) :
↑n m = n • m

See also `AddMonoid.End.natCast_def`.

source
@[simp]
theorem AddMonoid.End.ofNat_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) :
(OfNat.ofNat n) m = n • m
source
instance AddMonoid.End.instSemiring {M : Type uM} [AddCommMonoid M] :
Semiring (AddMonoid.End M)
Equations

- One or more equations did not get rendered due to their size.

source
instance AddMonoid.End.instRing {M : Type uM} [AddCommGroup M] :
Ring (AddMonoid.End M)
Equations

- One or more equations did not get rendered due to their size.