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] - chore(algebra/order/sub): split file #16868

Closed
wants to merge 119 commits into from
Closed

[Merged by Bors] - chore(algebra/order/sub): split file #16868

wants to merge 119 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Oct 8, 2022 •
edited by github-actions bot

@YaelDillies
initial commit
2a920a9
@YaelDillies
fix data.nat.basic
cde2f56
@YaelDillies
move bit0 lemmas
b5701d2
@YaelDillies
fix algebra.order.invertible
fb91c9a
@YaelDillies
fix instance
d26b779
@YaelDillies
fix data.set.intervals.instances
41e1ae1
@YaelDillies
primed versions of zero_lt_...
b427428
@YaelDillies
fix algebra.big_operators.order
eb82858
@YaelDillies
fix algebra.field_power
000a1cc
@YaelDillies
product instances
b04bd02
@YaelDillies
fix imports
df93015
@YaelDillies
actually fix imports
2209817
@YaelDillies
finally fix algebra.order.pi
e25be68
@YaelDillies
Merge remote-tracking branch 'origin/master' into ordered_semiring
55fff97
@YaelDillies
fix algebra.ring.prod
a6cb75e
@YaelDillies
reduce diff
94095dd
@YaelDillies
and even less diff
82d8d7f
@YaelDillies
less again
cc16585
@YaelDillies
fix algebra.order.field
82f099b
@YaelDillies
fix algebra.ring.prod
a8a806c
@YaelDillies
make nat lemmas intuitionistic again
e7ce422
@YaelDillies
ordered_cancel_comm_semiring.to_ordered_comm_semiring
2beea43
@YaelDillies
fix combinatorics.set_familty.kleitman
76ccacf
@YaelDillies
fix data.real.ennreal
56f34a0
@YaelDillies
Merge remote-tracking branch 'origin/master' into ordered_semiring
61f05a4
@YaelDillies
Merge remote-tracking branch 'origin/master' into ordered_semiring
19d59a2
@YaelDillies
delete linear_ordered_comm_ring.to_ordered_smul
cb8e36c
@YaelDillies
fix decidability again
8c83603
@YaelDillies
break long line
a549f16
@YaelDillies
fix algebra.order.positive.ring
43dc6ab
@semorrison semorrison 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. t-algebra Algebra (groups, rings, fields etc) labels Oct 8, 2022
@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 Oct 9, 2022
@semorrison semorrison 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 Oct 10, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Oct 13, 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 labels Oct 13, 2022
@semorrison
Copy link
Collaborator Author

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 Oct 13, 2022
@bors
Copy link

bors bot commented Oct 13, 2022

Canceled.

@semorrison
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Oct 13, 2022
@semorrison @YaelDillies
chore(algebra/order/sub): split file (#16868)
02b85de 

- [x] depends on: #16861

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


Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Oct 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/order/sub): split file [Merged by Bors] - chore(algebra/order/sub): split file Oct 13, 2022
@bors bors bot closed this Oct 13, 2022
@bors bors bot deleted the semorrison/split_algebra_order_group branch October 13, 2022 15:02
@eric-wieser eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Oct 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. hacktoberfest-accepted Without this label hacktoberfest is scared off by bors ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@semorrison @mathlib-dependent-issues-bot @jcommelin @eric-wieser @YaelDillies