Commit 2024-06-06 21:05 ac0ad78e

View on Github →

feat: Miscellaneous lemmas on quotienting by a polynomial (#11116) Adds modByMonic_eq_zero_iff_quotient_eq_zero and mk_singleton_eq

Estimated changes

Modified Mathlib/RingTheory/Ideal/Quotient.lean

added theorem Ideal.Quotient.mk_singleton_self

Modified Mathlib/RingTheory/Polynomial/Quotient.lean

added theorem Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero