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]
ha : a ≠ 0
n : ℕ
⊢ roots (↑(monomial n) a) = n • {0}
rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]