Degrees of derivatives under coefficient maps #
A coefficient map can lower the degree of a polynomial, and in positive characteristic it can
lower the degree of a derivative even when it preserves the degree of the polynomial itself.
Over an additively torsion-free target the second phenomenon cannot occur: preserving the degree
of p preserves the degree of p.derivative.
theorem
Polynomial.natDegree_map_derivative_eq_of_natDegree_map_eq
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
[IsAddTorsionFree S]
{f : R →+* S}
{p : Polynomial R}
(h : (map f p).natDegree = p.natDegree)
:
A coefficient map into an additively torsion-free semiring which preserves the degree of a polynomial also preserves the degree of its derivative.