Follow up from #9697: generalize nilpotent results to semirings

Even though one direction of Polynomial.isUnit_iff_coeff_isUnit_isNilpotent doesn't generalize to CommSemirings, Polynomial.coeff_isUnit_isNilpotent_of_isUnit does generalize and is sufficient to prove not_isUnit_of_degree_pos for reduced rings. The original proof doesn't quite work: it still suffices to show that the coefficients lie in every prime ideal, but you can't necessarily take the quotient by an ideal in a semiring and then argue in the resulting domain.

My proof is inspired by this answer, which shows if f is a unit and not a constant then its highest coefficient is nilpotent, and by induction on degree we just need to show f.eraseLead is also a unit. This follow from the general fact that if f+g is a unit and g is nilpotent in a CommSemiring, then f is a unit, with inverse given by $u=\sum\nolimits_{n=0}^{m-1} g^n v^{n+1}$, where v is the inverse of f+g and m is such that $g^m=0$. You can verify fu=1 by adding $g^m v^m=0$ to the end of $\sum\nolimits_{n=0}^{m-1}fg^n v^{n+1}$ and keep cancelling $f+g$ with $v$ until only one term (1) is left.

Some fun exercises that seem to missing in mathlib include: if a+b=0 in a CommSemiring then a^2=b^2, and if moreover a^n=0, then b^n=0.

cc @XavierXarles since he's interested in semirings ...

Originally posted by @alreadydone in https://github.com/leanprover-community/mathlib4/pull/9697#discussion_r1488731372

Start with the Polynomial.isUnit_iff_coeff_isUnit_isNilpotent and Polynomial.coeff_isUnit_isNilpotent_of_isUnit entries in Mathlib/RingTheory/Polynomial/Nilpotent.html, then review the discussion from #9697. Done means the applicable nilpotent coefficient result is generalized to CommSemirings and supports not_isUnit_of_degree_pos for reduced rings, with the proposed semiring lemmas covered.