Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/big-operators): some big operator lemmas#2152

Closed
b-mehta wants to merge 5 commits intomasterfrom
big-operator-lemmas
Closed

[Merged by Bors] - feat(algebra/big-operators): some big operator lemmas#2152
b-mehta wants to merge 5 commits intomasterfrom
big-operator-lemmas

Conversation

@b-mehta
Copy link
Copy Markdown
Collaborator

@b-mehta b-mehta commented Mar 14, 2020 •
edited
Loading

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

@b-mehta b-mehta added the awaiting-review The author would like community review of the PR label Mar 14, 2020
@b-mehta b-mehta changed the title big operator lemmas for combinatorics feat(algebra/big-operators): some big operator lemmas Mar 14, 2020
sgouezel
sgouezel reviewed Mar 15, 2020
View reviewed changes
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 15, 2020
jcommelin
jcommelin reviewed Mar 16, 2020
View reviewed changes
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Apr 3, 2020

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.

@b-mehta
Copy link
Copy Markdown
Collaborator Author

b-mehta commented Apr 12, 2020

I think all the suggestions are addressed!

@b-mehta b-mehta requested review from jcommelin and sgouezel April 12, 2020 00:01
@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 12, 2020
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Apr 12, 2020

@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.

jcommelin
jcommelin reviewed Apr 13, 2020
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a 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+

@bors
Copy link
Copy Markdown

bors bot commented Apr 13, 2020

✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@kim-em kim-em added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 13, 2020
@b-mehta @jcommelin
Apply suggestions from code review
a189d70 
Co-Authored-By: Johan Commelin <johan@commelin.net>
@b-mehta
Copy link
Copy Markdown
Collaborator Author

b-mehta commented Apr 13, 2020

bors r+

@bors
Copy link
Copy Markdown

bors bot commented Apr 13, 2020

👎 Rejected by label

@sgouezel sgouezel added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 13, 2020
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Apr 13, 2020

bors r+

bors bot pushed a commit that referenced this pull request Apr 13, 2020
@b-mehta
feat(algebra/big-operators): some big operator lemmas (#2152)
fe878ea 
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)
@bors
Copy link
Copy Markdown

bors bot commented Apr 13, 2020

Build succeeded

@bors
Copy link
Copy Markdown

bors bot commented Apr 13, 2020

Pull request successfully merged into master.

@bors bors bot changed the title feat(algebra/big-operators): some big operator lemmas [Merged by Bors] - feat(algebra/big-operators): some big operator lemmas Apr 13, 2020
@bors bors bot closed this Apr 13, 2020
@bors bors bot deleted the big-operator-lemmas branch April 13, 2020 19:58
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 15, 2020
@b-mehta @butterthebuddha
feat(algebra/big-operators): some big operator lemmas (leanprover-com…
4318ceb 
…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)
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 16, 2020
@b-mehta @butterthebuddha
feat(algebra/big-operators): some big operator lemmas (leanprover-com…
d9a9d7a 
…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)
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@b-mehta @cipher1024
feat(algebra/big-operators): some big operator lemmas (leanprover-com…
b69b228 
…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)
@YaelDillies YaelDillies mentioned this pull request Feb 10, 2025
Closed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@sgouezel sgouezel Awaiting requested review from sgouezel

2 more reviewers

@kim-em kim-em kim-em left review comments

@jcommelin jcommelin jcommelin left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@sgouezel sgouezel

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@b-mehta @sgouezel @kim-em @jcommelin @bryangingechen