mathlib3

76aee25d - refactor(big_operators/basic): move prod_mul_prod_compl (#6526)

refactor(big_operators/basic): move prod_mul_prod_compl (#6526) Several lemmas were unnecessarily in `src/data/fintype/card.lean`, and I've relocated them to `src/algebra/big_operators/basic.lean`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>