-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
[Merged by Bors] - feat(order/*): introduces complemented lattices #5747
Conversation
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry for the wait, let's get this merged.
bors r+
Defines `is_complemented` on bounded lattices Proves facts about complemented modular lattices Provides two instances of `is_complemented` on submodule lattices Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Defines `is_complemented` on bounded lattices Proves facts about complemented modular lattices Provides two instances of `is_complemented` on submodule lattices Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Defines
is_complemented
on bounded latticesProves facts about complemented modular lattices
Provides two instances of
is_complemented
on submodule lattices