theorem Polynomial.hasseDeriv_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} {k : ℕ} {p : Polynomial R} : (hasseDeriv k) (map f p) = map f ((hasseDeriv k) p)