Theorem MonomialOrder.sPolynomial_leadingTerm_mul

Modification history

2025-12-15 12:30

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` (#32788) …

Added MonomialOrder.sPolynomial_leadingTerm_mul View on Github →