Units in R[x]

Stream: new members

[Chengyan Hu]

Hi! I want to formalize the proposition that an element in R[x] ,where R is a commutative ring, is a unit if and only if its contant term is unit in R and all other coefficients are nilpotent in R. I check the leanexplore and didn’t find it. May I pleasely ask that if this result is already in mathlib or not?

[Damiano Testa]

Are you looking for docs#Polynomial.isUnit_iff_coeff_isUnit_isNilpotent ?

[Chengyan Hu]

Ahh that’s it! Thanks a lot!