Commit 2022-05-31 09:47 6531c720

chore(algebra/algebra/restrict_scalars): put a right action on restricted scalars (#13996) This provides module Rᵐᵒᵖ (restrict_scalars R S M) in terms of a module Sᵐᵒᵖ M action, by sending Rᵐᵒᵖ to Sᵐᵒᵖ through algebra_map R S. This means that restrict_scalars R S M now works for right-modules and bi-modules in addition to left-modules. This will become important if we change algebra R A to require A to be an R-bimodule, as otherwise restrict_scalars R S A would no longer be an algebra. Zulip