Commit 2025-12-04 15:25 478318e8

feat(Algebra/MvPolynomial/Equiv): degreeOf_eq_natDegree (#25926) Adds MvPolynomial.degreeOf_eq_natDegree, which states that the degree of a particular variable in a multivariate polynomial is equal to the degree of the single-variable polynomial obtained by treating the multivariable polynomial as a single variable polynomial over multivariable polynomials in the remaining variables. Also adds/refactors some relevant API around optionEquivLeft leading to the proof for this theorem, mainly by making analogous lemmas to those for finSuccEquiv. This PR continues the work from #12664.