-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/big-operators): some big operator lemmas #2152
Conversation
What is the status of this PR? The lemmas in there seem useful, and it looks like it only needs minor corrections to be merged. |
I think all the suggestions are addressed! |
@b-mehta, there are several open conversations above, from sgouezel --- could you either reply saying you've fixed them, or reply and click resolve conversation (assuming no further discussion is required). It's much easier for other reviewers who come along to work out where everything is up to. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Two minor comments. If you agree, please accept the two suggestions. After that, you can kick this on the merge queue by writing a comment bors r+
.
bors d+
✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-Authored-By: Johan Commelin <johan@commelin.net>
bors r+ |
👎 Rejected by label |
bors r+ |
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)
Build succeeded |
Pull request successfully merged into master. |
…munity#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)
…munity#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)
…munity#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)
Lemmas I found useful in my combinatorics project
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list