-
Notifications
You must be signed in to change notification settings - Fork 234
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: extend AddMonoidAlgebra.supDegree API #10355
Conversation
This is a part of #7173 that I hope will be uncontroversial. Co-authored-by: Junyan Xu <junyanxu.math@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.
LGTM!
(I did not check whether |
Co-authored-by: damiano <adomani@gmail.com>
|
||
variable [CovariantClass B B (· + ·) (· < ·)] [CovariantClass B B (Function.swap (· + ·)) (· < ·)] | ||
|
||
theorem apply_add_of_supDegree_eq (hD : D.Injective) {ap aq : A} |
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've definitely seen some form of this lemma. This probably means that you can use this lemma to golf a similar proof somewhere in the Polynomial.coeff_mul_of_degree_le
-range (made up name, but I have to go now!).
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.
LGTM. Let's merge this. Potential unlocked golfing can be done in a follow-up.
bors merge
This is a part of #7173 that I hope will be uncontroversial.
This PR was included in a batch that was canceled, it will be automatically retried |
This is a part of #7173 that I hope will be uncontroversial.
Build failed (retrying...): |
This is a part of #7173 that I hope will be uncontroversial.
Build failed (retrying...): |
This is a part of #7173 that I hope will be uncontroversial.
Build failed (retrying...): |
This is a part of #7173 that I hope will be uncontroversial.
Pull request successfully merged into master. Build succeeded: |
This is a part of #7173 that I hope will be uncontroversial.
This is a part of #7173 that I hope will be uncontroversial.
This is a part of #7173 that I hope will be uncontroversial.