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

[Merged by Bors] - feat(order/upper_lower): More prod lemmas#17747

Closed
YaelDillies wants to merge 4 commits intomasterfrom
upper_lower_prod_mono
Closed

[Merged by Bors] - feat(order/upper_lower): More prod lemmas#17747
YaelDillies wants to merge 4 commits intomasterfrom
upper_lower_prod_mono

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Nov 28, 2022 •
edited by github-actions bot
Loading

Transfer more set lemmas about prod to upper_set/lower_set lemmas.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-order Order hierarchy labels Nov 28, 2022
@YaelDillies YaelDillies mentioned this pull request Nov 28, 2022
Closed
1 task
@ghost ghost added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Nov 28, 2022
@ghost
Copy link
Copy Markdown

ghost commented Nov 29, 2022

This PR/issue depends on:

@eric-wieser eric-wieser added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 29, 2022
@YaelDillies YaelDillies removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 30, 2022
Vierkantor
Vierkantor approved these changes Dec 5, 2022
View reviewed changes
Copy link
Copy Markdown
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice work!

bors r+

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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-review The author would like community review of the PR labels Dec 5, 2022
bors bot pushed a commit that referenced this pull request Dec 5, 2022
@YaelDillies
feat(order/upper_lower): More prod lemmas (#17747)
97b62c8 
Transfer more `set` lemmas about `prod` to `upper_set`/`lower_set` lemmas.
@bors
Copy link
Copy Markdown

bors bot commented Dec 5, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/upper_lower): More prod lemmas [Merged by Bors] - feat(order/upper_lower): More prod lemmas Dec 5, 2022
@bors bors bot closed this Dec 5, 2022
@bors bors bot deleted the upper_lower_prod_mono branch December 5, 2022 17:04
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

2 more reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

@b-mehta b-mehta b-mehta approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YaelDillies @Vierkantor @b-mehta @eric-wieser @leanprover-community-bot-assistant