Commit 2021-12-21 16:21 cea1988f
View on Github →feat(data/finsupp/basic): add lemma disjoint_prod_add (#10799)
For disjoint finsupps f1 and f2, and function g, the product of the products of g over f1 and f2 equals the product of g over f1 + f2