mathlib3

feat(algebra/pointwise): More lemmas on pointwise multiplication

#997

Merged