no goals
R : Type u_2
S : Type u_1
F : Type ?u.679043
K : Type ?u.679046
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : Semiring S
φ : R →+* S
⊢ toPoly (map φ P) = Polynomial.map φ (toPoly P)
simp only [map, toPoly, map_C, map_X, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_pow]