Module structure and endomorphisms

In this file, we define Module.toAddMonoidEnd, which is (•) as a monoid homomorphism. We use this to prove some results on scalar multiplication by integers.

theorem AddMonoid.End.natCast_def {M : Type u_3} [AddCommMonoid M] (n : ℕ) : ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n

def Module.toAddMonoidEnd (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+* AddMonoid.End M

(•) as an AddMonoidHom.

This is a stronger version of DistribMulAction.toAddMonoidEnd

Equations

• Module.toAddMonoidEnd R M = { toMonoidHom := DistribMulAction.toAddMonoidEnd R M, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Module.toAddMonoidEnd_apply_apply (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (x : R) (x✝ : M) : ((toAddMonoidEnd R M) x) x✝ = x • x✝

def smulAddHom (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M

A convenience alias for Module.toAddMonoidEnd as an AddMonoidHom, usually to allow the use of AddMonoidHom.flip.

Equations

• smulAddHom R M = (Module.toAddMonoidEnd R M).toAddMonoidHom

@[simp]

theorem smulAddHom_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r : R) (x : M) : ((smulAddHom R M) r) x = r • x

theorem IsAddUnit.smul_left {S : Type u_2} {M : Type u_3} [AddCommMonoid M] {x : M} [Monoid S] [DistribMulAction S M] (hx : IsAddUnit x) (s : S) : IsAddUnit (s • x)

theorem IsAddUnit.smul_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} (x : M) (hr : IsAddUnit r) : IsAddUnit (r • x)

theorem AddMonoid.End.intCast_def (M : Type u_3) [AddCommGroup M] (z : ℤ) : ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z