mathlib3

d820a9d7 - feat(algebra/big_operators): some lemmas on big operators and `fin` (#7119)

feat(algebra/big_operators): some lemmas on big operators and `fin` (#7119) A couple of lemmas that I needed for `det_vandermonde` (#7116). I put them in a new file because I didn't see any obvious point that they fit in the import hierarchy. `big_operators/basic.lean` would be the alternative, but that file is big enough as it is. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>