Commit 2020-09-28 05:25 d77ac51c

chore(data/fintype/card): review API (#4287) API changes:

• finset.filter_mem_eq_inter now takes [Π i, decidable (i ∈ t)]; this way it works better with classical;
• add finset.mem_compl and finset.coe_compl;
• [DRY] drop finset.prod_range_eq_prod_fin and finset.sum_range_eq_sum_fin: use fin.prod_univ_eq_prod_range and fin.sum_univ_eq_sum_range instead;
• rename finset.prod_equiv to equiv.prod_comp to enable dot notation;
• add fintype.prod_dite: a specialized version of finset.prod_dite. Also golf a proof in analysis/normed_space/multilinear