mathlib3

feat(algebra/pointwise): pointwise scalar-multiplication lemmas

#1925

Merged