-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - lemmas about coeff for compute_degree
#15694
Conversation
Co-authored-by: Oliver Nash <github@olivernash.org>
…mmunity/mathlib into adomani_coeff_lemmas
Oliver, thank you very much for your comments: I implemented all of them! |
Co-authored-by: Oliver Nash <github@olivernash.org>
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!
I think it's worth adding one more lemma.
bors d+
|
||
variables [ring R] {p q : R[X]} | ||
|
||
lemma nat_degree_sub_le_iff_left (qn : q.nat_degree ≤ n) : |
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.
How about also adding the "right" version of this lemma:
lemma nat_degree_sub_le_iff_right (pn : p.nat_degree ≤ n) :
(p - q).nat_degree ≤ n ↔ q.nat_degree ≤ n :=
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.
Done! I also added the "symmetric" lemma
lemma nat_degree_sub : (p - q).nat_degree = (q - p).nat_degree :=
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
This PR proves 5 lemmas about `coeff`s of polynomials under products, multiplications, sums and differences. I also moved an already existing `ring` lemma to a previously non-existing section on `ring`. These lemmas are useful for the `compute_degree` tactic of #15691.
Pull request successfully merged into master. Build succeeded: |
compute_degree
compute_degree
This PR proves 5 lemmas about `coeff`s of polynomials under products, multiplications, sums and differences. I also moved an already existing `ring` lemma to a previously non-existing section on `ring`. These lemmas are useful for the `compute_degree` tactic of #15691.
This PR proves 5 lemmas about
coeff
s of polynomials under products, multiplications, sums and differences.I also moved an already existing
ring
lemma to a previously non-existing section onring
.These lemmas are useful for the
compute_degree
tactic of #15691.