mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: more API for AddMonoidAlgebra.supDegree / leadingCoeff / Monic

Open alreadydone opened this issue 2 years ago • 6 comments

Infrastructure for working with monomial orders on MvPolynomial rings. The lexicographic order is used in #6593 (proof of the fundamental theorem of symmetric polynomials)

Open in Gitpod

alreadydone avatar Sep 15 '23 03:09 alreadydone