mathlib

8b27c457 - feat(order/filter/pointwise): Missing pointwise operations (#13170)

feat(order/filter/pointwise): Missing pointwise operations (#13170) Define inversion/negation, division/subtraction, scalar multiplication/addition, scaling/translation, scalar subtraction of filters using the new `filter.map₂`. Golf the existing API.