Theorems · Definition · ring theory

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

Each element of the semiring defines a module endomorphism. This is a stronger version of DistribMulAction.toModuleEnd.

Defined in

Mathlib.Algebra.Module.LinearMap.End

Cited by

7 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleSemiringModuleSMulCommClass