Theorem MonomialOrder.sPolynomial_mul_monomial

Modification history

2025-12-15 12:30
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` (#32788) …
Deleted MonomialOrder.sPolynomial_mul_monomialView on Github →
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_monomialView on Github →
2025-12-04 18:52
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): add S-polynomial (#32344) …
Added MonomialOrder.sPolynomial_mul_monomialView on Github →