no goals
R : Type ?u.1111262
S : Type ?u.1111265
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.d = ↑φ P.a * -(x * y * z)
injection eq_sum_three_roots ha h3