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(analysis/special_functions/pow): rpow as an order_iso #10831

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(analysis/special_functions/pow): rpow as an order_iso #10831

wants to merge 5 commits into from

Conversation

j-loreaux
Copy link
Collaborator

@j-loreaux j-loreaux commented Dec 15, 2021 •
edited by github-actions bot

Bundles rpow into an order isomorphism on ennreal when the exponent is a fixed positive real.

Open in Gitpod

@j-loreaux j-loreaux added easy < 20s of review time. See the lifecycle page for guidelines. 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 Dec 15, 2021
@j-loreaux
Copy link
Collaborator Author

The dependence on #10701 isn't a strict requirement; it was just an easy way to prove the order isomorphism and I'm in no rush to have this result. I was going to use this bundled order isomorphism for another project, but didn't end up needing it. Thus I split off this PR to remove the dependence on #10701 for the other project.

@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. 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. merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Dec 22, 2021
@j-loreaux j-loreaux added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR labels Dec 22, 2021
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Dec 23, 2021
@urkud urkud 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 Dec 23, 2021
@j-loreaux j-loreaux added awaiting-CI The author would like to see what CI has to say before doing more work. 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 Dec 23, 2021
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Dec 23, 2021
@urkud
Copy link
Member

urkud commented Dec 23, 2021

Bors does something strange when the first commit in a PR is authored by someone else, so I suggest that you rebase on master and drop commits from my branch.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Dec 23, 2021
@github-actions
Copy link

This PR/issue depends on:

@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Dec 28, 2021
bors bot pushed a commit that referenced this pull request Dec 28, 2021
@j-loreaux @robertylewis
feat(analysis/special_functions/pow): rpow as an order_iso (#10831)
f11d3ca 
Bundles `rpow` into an order isomorphism on `ennreal` when the exponent is a fixed positive real.

- [x] depends on: #10701 


Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
@bors
Copy link

bors bot commented Dec 28, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions/pow): rpow as an order_iso [Merged by Bors] - feat(analysis/special_functions/pow): rpow as an order_iso Dec 28, 2021
@bors bors bot closed this Dec 28, 2021
@bors bors bot deleted the j-loreaux/rpow-order-iso branch December 28, 2021 22:59
erdOne pushed a commit that referenced this pull request Jan 1, 2022
@j-loreaux @robertylewis @erdOne
feat(analysis/special_functions/pow): rpow as an order_iso (#10831)
ab19dc1 
Bundles `rpow` into an order isomorphism on `ennreal` when the exponent is a fixed positive real.

- [x] depends on: #10701 


Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. easy < 20s of review time. See the lifecycle page for guidelines. 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
4 participants
@j-loreaux @urkud @robertylewis @jcommelin