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.

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

Equations

• AddMonoid.End.instAddMonoidWithOne M = { natCast := fun (n : ℕ) => n • 1, toAddMonoid := AddCommMonoid.toAddMonoid, toOne := AddMonoid.End.instOne M, natCast_zero := ⋯, natCast_succ := ⋯ }

@[simp]

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

See also AddMonoid.End.natCast_def.

@[simp]

theorem AddMonoid.End.ofNat_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) : (OfNat.ofNat n) m = n • m

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.

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.