mathlib3

9380977b - chore(algebra/big_operators/fin): moving lemmas (#13331)

chore(algebra/big_operators/fin): moving lemmas (#13331) This PR moves lemmas about products and sums over `fin n` from `data/fintype/card.lean` to `algebra/big_operators/fin.lean`. Co-authored-by: Oliver Nash <github@olivernash.org>