mathlib

bc7a201e - feat(*): Pointwise monoids have distributive negations (#14114)

feat(*): Pointwise monoids have distributive negations (#14114) More instances of `has_distrib_neg`: * `function.injective.has_distrib_neg`, `function.surjective.has_distrib_neg` * `add_opposite`, `mul_opposite` * `set`, `finset`, `filter`