Commit 2025-05-05 11:25 ba5ea6b9

View on Github →

feat(MvPolynomial): multiplicativity of totalDegree over domains (#24347)

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.degree_mem_support

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean

added theorem MvPolynomial.totalDegree_mul_of_isDomain