Commit 2025-12-10 17:42 f5f630e2

View on Github →

chore(RingTheory/MvPolynomial): weaken IsCancelMulZero to NoZeroDivisors in degree_mul and related lemmas. (#32558) As observed on Zulip NoZeroDivisors is a strictly weaker assumption than IsCancelMulZero.

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

modified theorem MonomialOrder.degree_mul'

modified theorem MonomialOrder.degree_mul

modified theorem MonomialOrder.degree_prod

modified theorem MonomialOrder.leadingCoeff_mul

modified theorem MonomialOrder.sPolynomial_mul_monomial

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean