Commit 2022-07-11 14:26 902e351c
View on Github →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.