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

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
⊢ (Ideal.Quotient.mk (Ideal.span {p})) p = 0
Tactic:
rw [Ideal.Quotient.eq_zero_iff_dvd]
State after:
no goals