Commit 2026-02-09 11:44 48c39f11
View on Github →feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypotheses of leadingCoeff_mul (#34765)
When f = 0 or g = 0, namely, the old hypothsese don't hold, m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g trivially holds.