feat(algebra/big-operators): some big operator lemmas (#2152)
Lemmas I found useful in my [combinatorics](https://b-mehta.github.io/combinatorics/) project
Make sure you have:
* [x] reviewed and applied the coding style: [coding](https://github.com/leanprover/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover/mathlib/blob/master/docs/contribute/naming.md)
* [x] reviewed and applied [the documentation requirements](https://github.com/leanprover/mathlib/blob/master/docs/contribute/doc.md)
* [x] make sure definitions and lemmas are put in the right files
* [x] make sure definitions and lemmas are not redundant
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: [code review check list](https://github.com/leanprover/mathlib/blob/master/docs/contribute/code-review.md)
