mathlib

54cc126b - feat(data/finset,data/fintype,algebra/big_operators): some more lemmas (#3124)

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`.)