English
If M is a left S-module, then RestrictScalars(R,S,M) carries a right Rᵐᵒᵖ-module structure via the standard construction using RingHom.op and the algebra map.
Русский
Если M — левый S-модуль, то RestrictScalars(R,S,M) обладает правым модулем над Rᵐᵒᵖ через стандартную конструкцию с RingHom.op и алгебраической связью.
LaTeX
$$$$ \\text{Module } (MulOpposite\\, R) (\\mathrm{RestrictScalars}(R,S,M)) $$$$
Lean4
/-- When `M` is a right-module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
right-module structure over `R`.
The preferred way of setting this up is
`[Module Rᵐᵒᵖ M] [Module Sᵐᵒᵖ M] [IsScalarTower Rᵐᵒᵖ Sᵐᵒᵖ M]`.
-/
instance opModule [Module Sᵐᵒᵖ M] : Module Rᵐᵒᵖ (RestrictScalars R S M) :=
letI : Module Sᵐᵒᵖ (RestrictScalars R S M) := ‹Module Sᵐᵒᵖ M›
Module.compHom M (RingHom.op <| algebraMap R S)
