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

[Merged by Bors] - chore(algebra/order/field): split out file about powers#17352

Closed
kim-em wants to merge 10 commits intomasterfrom
order_field_power
Closed

[Merged by Bors] - chore(algebra/order/field): split out file about powers#17352
kim-em wants to merge 10 commits intomasterfrom
order_field_power

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Nov 4, 2022 •
edited
Loading

This just pulls some material about powers of elements in linearly ordered fields into a separate file, as it isn't on the critical path to linear_ordered_field ℚ.

This will break in CI a few times as I find the downstream imports that need it.

Open in Gitpod

@kim-em kim-em 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. awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 4, 2022
@kim-em kim-em requested a review from a team as a code owner November 4, 2022 11:38
kim-em and others added 3 commits November 4, 2022 22:46
@ghost ghost 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 Nov 5, 2022
@ghost
Copy link
Copy Markdown

ghost commented Nov 5, 2022

This PR/issue depends on:

@kim-em kim-em added the awaiting-review The author would like community review of the PR label Nov 5, 2022
@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Nov 5, 2022

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 5, 2022

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

@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 awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 5, 2022
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Nov 5, 2022

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 Nov 5, 2022
bors bot pushed a commit that referenced this pull request Nov 6, 2022
@kim-em
chore(algebra/order/field): split out file about powers (#17352)
5cd9a65 
This just pulls some material about powers of elements in linearly ordered fields into a separate file, as it isn't on the critical path to `linear_ordered_field ℚ`.

This will break in CI a few times as I find the downstream imports that need it.

- [x] depends on: #17350


[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Nov 6, 2022
@kim-em
chore(algebra/order/field): split out file about powers (#17352)
f8f8be9 
This just pulls some material about powers of elements in linearly ordered fields into a separate file, as it isn't on the critical path to `linear_ordered_field ℚ`.

This will break in CI a few times as I find the downstream imports that need it.

- [x] depends on: #17350


[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 6, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/order/field): split out file about powers [Merged by Bors] - chore(algebra/order/field): split out file about powers Nov 6, 2022
@bors bors bot closed this Nov 6, 2022
@bors bors bot deleted the order_field_power branch November 6, 2022 05:43
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. 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.

2 participants

@kim-em @PatrickMassot