Theorems · Definition · ring theory

DistribSMul.toLinearMap

(R : Type u_1) →
  {S : Type u_3} →
    (M : Type u_4) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : DistribSMul S M] → [SMulCommClass S R M] → S → M →ₗ[R] M

Each element of the monoid defines a linear map. This is a stronger version of DistribSMul.toAddMonoidHom.

Defined in

Mathlib.Algebra.Module.LinearMap.End

Cited by

50 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidModuleDistribSMulSMulCommClass