-
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
feat(algebra/order_operation_defs): introduce new typeclasses for mixing orders and binary operations #7396
Conversation
following Sébastien's and Eric's suggestions
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 otherwise, thank you!
-- TODO: convert `has_exists_mul_of_le`, `has_exists_add_of_le`? | ||
-- TODO: relationship with add_con | ||
-- include equivalence of `left_cancel_semigroup` with | ||
-- `semigroup partial_order contravariant_class α α (*) (≤)`? | ||
-- use ⇒, as per Eric's suggestion? |
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.
Are these TODOs for a later PR, or for iterations of this one?
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.
I am planning to take these on, though I had been experimenting with a newer PR. I will get back to working on this next week.
|
||
lemma is_symm_op.swap_eq {α β} (op) [is_symm_op α β op] : flip op = op := | ||
funext $ λ a, funext $ λ b, (is_symm_op.symm_op a b).symm |
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.
This belongs somewhere way more basic; perhaps function.basic
or even logic.basic
.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Dear Anne and Eric, Thank you for your comments! I will take a look at this PR again next week and will get back to you! |
This can be closed now, right? |
This PR revises and splits off the definitions of PR #7371.
I introduce two definitions, like in the other PR:
covariant
andcontravariant
. They are definitions instead of classes since, if I understood correctly, Sébastien said that they would burden the typeclass search system.Using these definitions, I then introduce 16 new classes, each one saying that addition/multiplication is left/right monotone in various convenient ways. They system is heavily based on the original
ordered_[...]
hierarchy, except that now it is possible to mix-and-match assumptions on the algebraic side and on the order side.I also provide instances to show that
(≤)
assumptions imply(<)
assumptions, if the order is linear.Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered.20stuff