Theorem MonomialOrder.degree_mul'

Modification history

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.degree_mul'View on Github →
2025-12-02 10:19
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): add two lemmas about degree (#32336) …
Added MonomialOrder.degree_mul'View on Github →