mathlib

902e351c - feat(data/set/pointwise): `list` and `multiset` versions of n-ary lemmas (#14928)

feat(data/set/pointwise): `list` and `multiset` versions of n-ary lemmas (#14928) These lemmas are generalizations of the existing lemmas about `finset.prod` and `finset.sum`, but for the `list` and `multiset` versions. The finset ones can now be proved in terms of the multiset ones.