Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(data/real/ennreal): Order properties of addition #13371

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(data/real/ennreal): Order properties of addition #13371

wants to merge 5 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Apr 11, 2022 •
edited by joneugster

Inherit algebraic order lemmas from with_top. Also protect ennreal.add_lt_add_iff_left and ennreal.add_lt_add_iff_right, as they should have been.

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Apr 11, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 11, 2022
@YaelDillies YaelDillies mentioned this pull request Apr 12, 2022
Closed
4 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 16, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies YaelDillies added the easy < 20s of review time. See the lifecycle page for guidelines. label Apr 17, 2022
b-mehta
b-mehta reviewed Apr 17, 2022
View reviewed changes
src/data/real/ennreal.lean Outdated Show resolved Hide resolved
@b-mehta b-mehta removed the easy < 20s of review time. See the lifecycle page for guidelines. label Apr 17, 2022
@b-mehta
Copy link
Collaborator

b-mehta commented Apr 18, 2022

bors merge

@github-actions github-actions bot 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 Apr 18, 2022
bors bot pushed a commit that referenced this pull request Apr 18, 2022
@YaelDillies
feat(data/real/ennreal): Order properties of addition (#13371)
5c75390 
Inherit algebraic order lemmas from `with_top`. Also protect `ennreal.add_lt_add_iff_left` and `ennreal.add_lt_add_iff_right`, as they should have been.
@bors
Copy link

bors bot commented Apr 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/real/ennreal): Order properties of addition [Merged by Bors] - feat(data/real/ennreal): Order properties of addition Apr 18, 2022
@bors bors bot closed this Apr 18, 2022
@bors bors bot deleted the ennreal_add_lt_add branch April 18, 2022 19:11
@YaelDillies YaelDillies mentioned this pull request Feb 6, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@b-mehta b-mehta b-mehta left review comments

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+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @leanprover-community-bot-assistant @b-mehta