Commit 2022-07-22 22:11 1e024cb6

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.