Commit 2020-05-20 15:35 4c3e1a9d
View on Github →feat(algebra): the R-module structure on S-linear maps, for S an R-algebra (#2759) I couldn't find this already in mathlib, but perhaps I've missed it.
feat(algebra): the R-module structure on S-linear maps, for S an R-algebra (#2759) I couldn't find this already in mathlib, but perhaps I've missed it.