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

source
theorem AddMonoid.End.natCast_def {M : Type u_3} [AddCommMonoid M] (n : ℕ) :
↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n
source
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' := ⋯ }

Instances For

source
@[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✝
source
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

Instances For

source
@[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
source
theorem IsAddUnit.smul_left {S : Type u_2} {M : Type u_3} [AddCommMonoid M] {x : M} [DistribSMul S M] (hx : IsAddUnit x) (s : S) :
IsAddUnit (s • x)
source
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)
source
theorem AddMonoid.End.intCast_def (M : Type u_3) [AddCommGroup M] (z : ℤ) :
↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z