[Merged by Bors] - feat(data.polynomial.div): add theorem X_pow_dvd_iff

[faenuccio]

Add the theorem X_pow_dvd_iff saying that a polynomial is divisible by $X^n$ if and only if its first $(n-1)$ coefficients are $0$.

---

[Vierkantor]

Thanks!

bors d+

[bors]

✌️ faenuccio can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[faenuccio]

Thanks!

bors d+

OK, I think this works but since there were changes I am not delegated any more to merge.

[eric-wieser]

bors merge

Note that bors would definitely have allowed you to merge this yourself; and certainly I think @Vierkantor's intent was for you to do so, but no harm in being cautious!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[faenuccio]

bors merge

Note that bors would definitely have allowed you to merge this yourself; and certainly I think @Vierkantor's intent was for you to do so, but no harm in being cautious!

Oh, I see, I thought that the delegation was only for one commit, and then if successive commits were added (as in this case) it would lose its value. Because the red warning "you are not able to merge" was back again after I pushed new commits. I will try on another PR! Thanks.