mathlib

1e024cb6 - feat(data/polynomial/degree/definitions): redefine `polynomial.degree` as `p.support.max` (#15199)

feat(data/polynomial/degree/definitions): redefine `polynomial.degree` as `p.support.max` (#15199) This PR redefines `polynomial.degree p`: * old: `p.support.sup coe` * new: `p.support.max`. The two definitions are defeq and relatively few changes are required. Weirdness: `open finset` seems to no longer work consistently. This is the largest source of differences. In particular, the file `ring_theory/polynomial/cyclotomic/basic` only changed because I added `finset.` in several places.