[Merged by Bors] - refactor(algebra/group/defs): remove left-right_cancel_comm_monoids #7134
Conversation
adomani
added
the
awaiting-review
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 |
urkud
changed the title
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: |
bors
bot
changed the title
adomani
removed
the
awaiting-review
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_monoidrequires 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