Commit 2023-08-02 16:24 8368c269
View on Github →feat: generalize scalars in Algebra.lsmul (#6209)
This generalizes from Algebra.lsmul R M : A →ₐ[R] Module.End R M to Algebra.lsmul R S M : A →ₐ[R] Module.End S M.
This generalization was previously not possible because Module.End S M was not an R-algebra.
Notably this now allows things like Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A (right multiplication).
This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality.
Instead, we just replace Algebra.lsmul R with Algebra.lsmul R R.