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: pointwise scalar multiplication is monotone #11809
Conversation
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
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.
Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
||
variable {ι : Sort*} {M α : Type*} | ||
|
||
theorem smul_mono_right [SMul M α] [Preorder α] [CovariantClass M α HSMul.hSMul LE.le] |
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.
Can you add a version with the gcongr
attribute (I think it has to be formulated separately using \le
).
bors d+
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
apparently the label bot doesn't work from comments to the code. |
bors merge |
Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.
Pull request successfully merged into master. Build succeeded: |
Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.
Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.
Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.
Everywhere we have a `smul_mem_pointwise_smul` lemma, I've added this result.
Everywhere we have a
smul_mem_pointwise_smul
lemma, I've added this result.Should this be stated with a typeclass? If so, what's the API lemma that recovers this result?done