mathlib3

5329bf3a - feat(algebra/pointwise): More lemmas on pointwise multiplication (#997)

feat(algebra/pointwise): More lemmas on pointwise multiplication (#997) * feat(algebra/pointwise): More lemmas on pointwise multiplication * Fix build, hopefully * Fix build * to_additive + fix formatting