Theorems · Definition · commutative algebra

Module.restrictScalars

(R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid M] → [inst_2 : CommSemiring R] → [Algebra R S] → [Module S M] → Module R M

When M is a module over a ring S, and S is an algebra over R, then M inherits a module structure over R. Not an instance because S cannot be inferred. The preferred way of setting this up is [Module R M] [Module S M] [IsScalarTower R S M].

Defined in

Mathlib.Algebra.Algebra.RestrictScalars

Cited by

3 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

SemiringAddCommMonoidCommSemiringAlgebraModule