Commit 2024-12-04 05:57 ea515836

feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders (#19454) Formalize the division algorithm with respect to a monomial order This is part of an ongoing work to formalize Groebner theory. For the moment, only the lexicographic order is present in mathlib, but subsequent PRs will introduce the homogeneous lexicographic order and the homogeneous reverse lexicographic order.