Commit 2020-06-22 16:12 54cc126b

feat(data/finset,data/fintype,algebra/big_operators): some more lemmas (#3124) Add some finset, fintype and algebra.big_operators lemmas that were found useful in proving things related to affine independent families. (In all cases where results are proved for products, and then derived for sums where possible using to_additive, it was the result for sums that I actually had a use for. In the case of eq_one_of_card_le_one_of_prod_eq_one and eq_zero_of_card_le_one_of_sum_eq_zero, to_additive couldn't be used because it also tries to convert the 1 in s.card ≤ 1 to 0.)