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(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition #14529
Conversation
… and lie subalgebras form canonically ordered additivve monoids under addition
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.
bors d+
I think we should make this an instance - and remove the simp lemma - globally.
You can do that in a subsequent PR, if you want.
local attribute [instance] canonically_ordered_add_monoid | ||
``` | ||
-/ | ||
def canonically_ordered_add_monoid : canonically_ordered_add_monoid (submodule R M) := |
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.
make reducible (see reducible non-instance library note)
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'm not sure I agree; I thought @[reduclble] foo
was for when we have instance : X := foo
, not for when we have local attribute [instance] foo
.
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.
At any rate, the follow-up PR will make this moot.
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Done in #14553 |
bors merge |
… and lie subalgebras form canonically ordered additive monoids under addition (#14529) We can't actually make these instances because they result in loops for `simp`. The `le_iff_exists_sup` lemma is probably not very useful for much beyond these new instances, but it matches `le_iff_exists_add`.
Pull request successfully merged into master. Build succeeded: |
… and lie subalgebras form canonically ordered additive monoids under addition (#14529) We can't actually make these instances because they result in loops for `simp`. The `le_iff_exists_sup` lemma is probably not very useful for much beyond these new instances, but it matches `le_iff_exists_add`.
We can't actually make these instances because they result in loops for
simp
.The
le_iff_exists_sup
lemma is probably not very useful for much beyond these new instances, but it matchesle_iff_exists_add
.