mathlib3
feat(topology/algebra/group): define filter pointwise addition
#1215
Merged
Merged