mathlib3

4c3e1a9d - feat(algebra): the R-module structure on S-linear maps, for S an R-algebra (#2759)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>