no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
ha : a ≠ 0
⊢ roots (↑C a * p) = roots p
by_cases hp : p = 0 <;>
  simp only [roots_mul, *, Ne.def, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
    zero_add, MulZeroClass.mul_zero]