mathlib

fc19a4e4 - feat({data/finset,order/filter}/pointwise): Multiplicative action on pointwise monoids (#14214)

feat({data/finset,order/filter}/pointwise): Multiplicative action on pointwise monoids (#14214) `mul_action`, `distrib_mul_action`, `mul_distrib_mul_action` instances for `finset` and `filter`. Also delete `set.smul_add_set` because `smul_add` proves it.