no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
H : x = 0
⊢ roots (↑C x) = 0
rw [H, C_0, roots_zero]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
H : ¬x = 0
r : R
⊢ count r (roots (↑C x)) = count r 0
rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)]