mathlib3

fa2cb8a9 - feat(data/set/pointwise/big_operators): image distributes across pointwise big operators (#18840)

feat(data/set/pointwise/big_operators): image distributes across pointwise big operators (#18840) The main results here are: * `set.image_finset_prod : f '' (∏ i in m, s i) = (∏ i in m, f '' s i)`, which says that the image under a monoid morphism commutes with the pointwise n-ary product of sets * `set.image_finset_prod_pi : (λ f : ι → α, ∏ i in l, f i) '' (l : set ι).pi S = (∏ i in l, S i)`, which says that turning a family of sets into a set of families and taking the product over each family is the same as taking the pointwise product. Both are n-ary versions of existing binary results.