Commit 2022-05-21 08:14 fc19a4e4
View on Github →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.