Commit 2024-05-22 13:33 b0729237

feat(Mathlib.Algebra.Polynomial.RingDivision): add Polynomial.nmem_nonZeroDivisors_iff (#12950) We add Polynomial.nmem_nonZeroDivisors_iff, known as McCoy's theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

• depends on: #12958