rw [Polynomial.modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p.modByMonic q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0
no goals