no goals
A : Type ?u.35822
K : Type ?u.35825
R : Type u_1
S : Type ?u.35831
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
⊢ natDegree (scaleRoots p s) = natDegree p
simp only [natDegree, degree_scaleRoots]