no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ roots (↑normalize p) = roots p
rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]