Commit 2020-04-13 17:33 fe878eaf

feat(algebra/big-operators): some big operator lemmas (#2152) Lemmas I found useful in my combinatorics project Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• 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