no goals
A : Type ?u.36545
K : Type ?u.36548
R : Type u_1
S : Type ?u.36554
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
⊢ Monic (scaleRoots p s) ↔ Monic p
simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]