mathlib

cea1988f - feat(data/finsupp/basic): add lemma `disjoint_prod_add` (#10799)

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`