Theorem: Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero (FormalSnarksProject/ToMathlib/PolynomialQuotient.lean)

State before:
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
Tactic:
rw [Polynomial.modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]
State after:
no goals