[Merged by Bors] - feat: units of polynomial rings #4691
Conversation
EmilieUthaiwat
changed the title
|
This is my first pull request so I apologize in advance if it is not done correctly. |
EmilieUthaiwat
added
awaiting-review
| @@ -11,6 +11,7 @@ Authors: Oliver Nash | |||
| import Mathlib.Data.Nat.Choose.Sum | |||
| import Mathlib.Algebra.Algebra.Bilinear | |||
| import Mathlib.RingTheory.Ideal.Operations | |||
| import Mathlib.Algebra.GeomSum | |||
There was a problem hiding this comment.
How much extra does this pull in?
There was a problem hiding this comment.
Mathlib.Algebra.GeomSum imports the following files:
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Tactic.Abel
import Mathlib.Data.Nat.Parity
Mathlib.RingTheory.Nilpotent already pulls in every file mentioned above, except Mathlib.Data.Nat.Parity, so the only new file imported by Mathlib.Algebra.GeomSum is Mathlib.Data.Nat.Parity.
|
Otherwise LGTM. |
|
Thank you! |
|
Is there anything else that I should do concerning this PR? |
|
@semorrison I don't see any reason not to merge this, but I'm not doing a maintainer merge in case you wanted to wait. |
ADedecker
added
awaiting-author
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
riccardobrasca
added
awaiting-review
|
|
||
| /-- Let `P` be a polynomial over `R`. If `P` is a unit, then all its coefficients are nilpotent, | ||
| except its constant term which is a unit. -/ | ||
| theorem coeff_isUnit_isNilpotent_of_isUnit {P : Polynomial R} (hunit : IsUnit P) : |
There was a problem hiding this comment.
In this case the previous name was fine. I don't really have a preference, so keep the one you prefer.
|
Thanks and congratulations for your first PR! 🎉 |
|
🚀 Pull request has been placed on the maintainer queue by ADedecker. |
|
bors r+ |
github-actions
bot
added
ready-to-merge
We proved that a polynomial is a unit if and only if all of its coefficients are nilpotent, except the constant term which is a unit. Co-authored-by: Cyprien Chauveau cyprien.chauveau@etu.u-paris.fr Co-authored-by: Lucas Pouillart lucas.pouillart@etu.u-paris.fr Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
We proved that a polynomial is a unit if and only if all of its coefficients are nilpotent, except the constant term which is a unit. Co-authored-by: Cyprien Chauveau cyprien.chauveau@etu.u-paris.fr Co-authored-by: Lucas Pouillart lucas.pouillart@etu.u-paris.fr Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
We proved that a polynomial is a unit if and only if all of its coefficients are nilpotent, except the constant term which is a unit. Co-authored-by: Cyprien Chauveau cyprien.chauveau@etu.u-paris.fr Co-authored-by: Lucas Pouillart lucas.pouillart@etu.u-paris.fr Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
We proved that a polynomial is a unit if and only if all of its coefficients are nilpotent, except the constant term which is a unit.
Co-authored-by: Cyprien Chauveau cyprien.chauveau@etu.u-paris.fr
Co-authored-by: Lucas Pouillart lucas.pouillart@etu.u-paris.fr
I can backport this to mathlib3 if needed.