Commit 2025-12-15 12:30 103af122
View on Github →feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of sPolynomial_mul_monomial (#32788)
This commit adds a variant sPolynomial_mul_monomial', using m.degree (monomial d c * p) instead of d + m.degree p, which are different in the edge case that one of c and p is 0.
A pair of variants about leadingTerm instead of monomial are also added.