no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p✝ q p : R[X]
hq : Monic q
⊢ p %ₘ q = p %ₘ (q * ↑C (leadingCoeff q)⁻¹)
simp only [Monic.def.1 hq, inv_one, mul_one, C_1]