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 →