-
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] - refactor(algebra/group/defs): remove left-right_cancel_comm_monoids #7134
Conversation
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Thanks, Anne: I pushed your suggestions! |
I'll push a few fixes soon (UPD: done). The most important: |
bors d+ |
Yury, thank you very much for the fixes! Is the guiding principle that you want to have as few fields as possible? So no need to assume right cancel, given left and comm? |
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
remove `mul_right_cancel` from ordered_cancel_comm_monoid
remove `mul_right_cancel` from linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid
remove `mul_right_cancel` from ordered_comm_group.to_ordered_cancel_comm_monoid
remove several add_right_cancel
Yes, users who define instances should have to provide as few fields as possible. We don't follow this rule everywhere (e.g., the axioms for |
Wow, Yury: at this rate, mathlib will be less than half its size in a matter of hours! Thank you so much for the changes: I thought that they were going to be all simple removal of unneeded fields, but it would have taken me quite a while to fix some of these errors! Thanks for all your help! I imagine that, as soon as the PR builds successfully it can be merged, right? |
bors r+ |
…7134) There were 6 distinct classes * `(add_)left_cancel_comm_monoid`, * `(add_)right_cancel_comm_monoid`, * `(add_)cancel_comm_monoid`. I removed them all, except for the last 2: * `(add_)cancel_comm_monoid`. The new typeclass `cancel_comm_monoid` requires only `a * b = a * c → b = c`, and deduces the other version from commutativity. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
There were 6 distinct classes
(add_)left_cancel_comm_monoid
,(add_)right_cancel_comm_monoid
,(add_)cancel_comm_monoid
.I removed them all, except for the last 2:
(add_)cancel_comm_monoid
.The new typeclass
cancel_comm_monoid
requires onlya * b = a * c → b = c
, and deduces the other version from commutativity.Please, can you really make sure that I have not messed up? Thanks! In particular, I have moved the
attribute [to_additive]
after the various typeclasses in question (UPD: Yury moved them back). For more information, see the Zulip discussion.Many thanks to Anne, Eric, Kevin and Mario for their explanations! I have made an effort to understand them, but large parts of them are still mysterious to me!
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/mul_right_comm_monoid
Co-authored-by: Yury G. Kudryashov urkud@urkud.name