Commit 2025-07-03 08:10 9162a4a8

feat(Algebra/Polynomial/Degree/IsMonicOfDegree): new file (#26507) This adds a predicate Polynomial.IsMonicOfDegree p n expressing that the polynomial p is monic and has natDegree equal to n and provides some API for it. Bundling the two properties is quite convenient (e.g., showing that the product of two monic polynomials of degrees m and n is monic of degree m+n needs a few lines with the currently available API) and proved very helpful for formalizing a proof of the Gelfand-Mazur theorem over the reals. See also here on Zulip : #mathlib4 > Gelfand-Mazur theorem @ 💬.