-
Notifications
You must be signed in to change notification settings - Fork 297
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] - fix(algebra/ordered_monoid): Ensure that ordered_cancel_comm_monoid
can provide a cancel_comm_monoid
instance
#5713
Conversation
… can provide a `cancel_comm_monoid` instance
src/algebra/group/defs.lean
Outdated
@@ -285,7 +285,7 @@ class add_cancel_comm_monoid (M : Type u) | |||
extends add_left_cancel_comm_monoid M, add_right_cancel_comm_monoid M | |||
|
|||
/-- Commutative version of cancel_monoid. -/ | |||
@[protect_proj, ancestor right_cancel_comm_monoid left_cancel_comm_monoid, to_additive add_cancel_comm_monoid] | |||
@[protect_proj, ancestor left_cancel_comm_monoid right_cancel_comm_monoid, to_additive add_cancel_comm_monoid] |
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.
Turns out that by getting this backwards, to_additive
would map to_left_cancel_comm_monoid
to to_add_right_cancel_comm_monoid
! The order matters.
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.
Perhaps we should add a warning about this to the to_additive
doc entry?
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.
Sounds like a job for #5338
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.
Yes, fair enough.
Thanks!
bors r+
… can provide a `cancel_comm_monoid` instance (#5713)
Pull request successfully merged into master. Build succeeded: |
ordered_cancel_comm_monoid
can provide a cancel_comm_monoid
instanceordered_cancel_comm_monoid
can provide a cancel_comm_monoid
instance
… can provide a `cancel_comm_monoid` instance (#5713)
Zulip