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

feat: port order.galois_connection #1093

Closed
wants to merge 1 commit into from
Closed

feat: port order.galois_connection #1093

wants to merge 1 commit into from

Conversation

PatrickMassot
Copy link
Member

@PatrickMassot PatrickMassot commented Dec 18, 2022 •
edited

Do not work on this PR yet, the mathlib3port version used doesn't have Order.CompleteLattive alignments.

@PatrickMassot PatrickMassot added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 18, 2022
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 20, 2022
@semorrison
Copy link
Contributor

Done in #1099.

@semorrison semorrison closed this Dec 20, 2022
@int-y1 int-y1 deleted the order_galois_connection branch April 16, 2023 18:34
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
mathlib-port This is a port of a theory file from mathlib. merge-conflict The PR has a merge conflict with master, and needs manual merging. WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@PatrickMassot @semorrison