Theorem MonomialOrder.degree_mem_support

Modification history

2025-05-05 11:25
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(MvPolynomial): multiplicativity of `totalDegree` over domains (#24347)
Added MonomialOrder.degree_mem_supportView on Github →