English
If M is a module over S and S is an algebra over R, then RestrictScalars(R,S,M) inherits a natural Module R-structure via composition with the algebra map.
Русский
Если M — модуль над S, и S является алгеброй над R, то RestrictScalars(R,S,M) наследует естественную структуру модуля над R через композицию с алгебраической связью.
LaTeX
$$$$ \\text{Module } R (\\mathrm{RestrictScalars}(R,S,M)) $$$$
Lean4
/-- When `M` is a module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
module structure over `R`.
The preferred way of setting this up is `[Module R M] [Module S M] [IsScalarTower R S M]`.
-/
instance module [Module S M] : Module R (RestrictScalars R S M) :=
Module.compHom M (algebraMap R S)
