Commit 2025-12-02 10:19 d822606b
View on Github →feat(RingTheory/MvPolynomial/MonomialOrder): add two lemmas about degree (#32336) It is used by and split from https://github.com/leanprover-community/mathlib4/pull/29203.
feat(RingTheory/MvPolynomial/MonomialOrder): add two lemmas about degree (#32336) It is used by and split from https://github.com/leanprover-community/mathlib4/pull/29203.