Theorem MonomialOrder.sPolynomial_mul_monomial

Modification history

2025-12-10 17:42

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

chore(RingTheory/MvPolynomial): weaken IsCancelMulZero to NoZeroDivisors in `degree_mul` and related lemmas. (#32558) …

Modified MonomialOrder.sPolynomial_mul_monomial View on Github →

2025-12-04 18:52

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

feat(RingTheory/MvPolynomial/MonomialOrder): add S-polynomial (#32344) …

Added MonomialOrder.sPolynomial_mul_monomial View on Github →