mathlib

12fde093 - feat(data/finset/finsupp): Finitely supported product of finsets (#11639)

feat(data/finset/finsupp): Finitely supported product of finsets (#11639) Define * `finsupp.indicator`: Similar to `finsupp.on_finset` except that it only requires a partially defined function. This is more compatible with `finset.pi`. * `finset.finsupp : finset ι → (ι → finset α) → finset (ι →₀ α)`: Finitely supported product of finsets. * `finsupp.pi : (ι →₀ finset α) → finset (ι →₀ α)`: The set of finitely supported functions whose `i`-th value lies in the `i`-th of a given `finset`-valued `finsupp`.