Theorems · Definition · ring theory

AddMonoidHom.smul

{R : Type u_1} → {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R →+ M →+ M

Scalar multiplication as a biadditive monoid homomorphism. We need M to be commutative to have addition on M →+ M.

Defined in

Mathlib.Algebra.Module.Hom

Cited by

2 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule