Theorems · Definition · ring theory

DistribMulAction.toModuleEnd

(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 : Monoid S] → [inst_4 : DistribMulAction S M] → [SMulCommClass S R M] → S →* Module.End R M

Each element of the monoid defines a module endomorphism. This is a stronger version of DistribMulAction.toAddMonoidEnd.

Defined in

Mathlib.Algebra.Module.LinearMap.End

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleMonoidDistribMulActionSMulCommClass