Skip to content

feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypothesis#38323

Open
NoahW314 wants to merge 1 commit intoleanprover-community:masterfrom
NoahW314:leadingTerm
Open

feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypothesis#38323
NoahW314 wants to merge 1 commit intoleanprover-community:masterfrom
NoahW314:leadingTerm

Commits

Commits on Apr 21, 2026