R : Type u_1
S : Type ?u.683267
F : Type ?u.683270
K : Type ?u.683273
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain R
h0 : toPoly P ≠ 0
x : R
⊢ eval x (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
R : Type u_1
S : Type ?u.683267
F : Type ?u.683270
K : Type ?u.683273
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain R
h0 : toPoly P ≠ 0
x : R
⊢ x ∈ roots P ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
rw [roots, mem_roots h0, IsRoot, toPoly]
no goals
R : Type u_1
S : Type ?u.683267
F : Type ?u.683270
K : Type ?u.683273
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain R
h0 : toPoly P ≠ 0
x : R
⊢ eval x (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]