Theorems · Definition · commutative algebra

RestrictScalars.lsmul

(R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Algebra R S] → [inst_4 : Module S M] → S →ₐ[R] Module.End R (RestrictScalars R S M)

The R-algebra homomorphism from the original coefficient algebra S to endomorphisms of RestrictScalars R S M.

Defined in

Mathlib.Algebra.Algebra.RestrictScalars

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidCommSemiringAlgebraModule