no goals
R : Type u_2
S : Type u_1
F : Type ?u.681619
K : Type ?u.681622
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ roots (map φ P) = Polynomial.roots (Polynomial.map φ (toPoly P))
rw [roots, map_toPoly]