Commit 2021-04-14 23:14 d820a9d7

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.