no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : (X - ↑C a) * (p /ₘ (X - ↑C a)) = p
⊢ IsRoot p a
rw [← h, IsRoot.def, eval_mul, eval_sub, eval_X, eval_C, sub_self, MulZeroClass.zero_mul]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : eval a p = 0
⊢ (X - ↑C a) * (p /ₘ (X - ↑C a)) = p
conv_rhs =>
    rw [← modByMonic_add_div p (monic_X_sub_C a)]
    rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]