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]
r a : R
⊢ rootMultiplicity a (↑C r) = 0
simp only [rootMultiplicity_eq_zero_iff, IsRoot, eval_C, C_eq_zero, imp_self]