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] - refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file #10165

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file #10165

wants to merge 4 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Feb 1, 2024 •
edited

This reworks the location of the lemmas from #10086, by moving them to a new Mathlib.Order.CompactlyGenerated.Intervals file.
The existing Mathlib.Order.CompactlyGenerated is moved to Mathlib.Order.CompactlyGenerated.Basic for consistency.

Open in Gitpod

@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI labels Feb 1, 2024
@eric-wieser eric-wieser mentioned this pull request Feb 1, 2024
Closed
2 tasks
ocfnash
ocfnash approved these changes Feb 1, 2024
View reviewed changes
Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thank you for doing this.

I suggest going one step further and also replacing Mathlib.Order.CompactlyGenerated with Mathlib.Order.CompactlyGenerated.Basic.

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Feb 1, 2024

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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Feb 1, 2024
@ocfnash
Copy link
Contributor

ocfnash commented Feb 1, 2024

@eric-wieser if you like you can give the "auto-merge-after-CI" label a whirl here.

@eric-wieser eric-wieser changed the title refactor: move lemmas with a multiset dependency to a new file refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file Feb 1, 2024
@eric-wieser eric-wieser added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 1, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2024
@eric-wieser
refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset…
e64d0a1 
… dependency to a new file (#10165)

This reworks the location of the lemmas from #10086, by moving them to a new `Mathlib.Order.CompactlyGenerated.Intervals` file.
The existing `Mathlib.Order.CompactlyGenerated` is moved to `Mathlib.Order.CompactlyGenerated.Basic` for consistency.
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file [Merged by Bors] - refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file Feb 1, 2024
@mathlib-bors mathlib-bors bot closed this Feb 1, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/compact-intervals branch February 1, 2024 20:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees
No one assigned
Labels
auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@eric-wieser @ocfnash @leanprover-community-mathlib4-bot