mathlib3

0e72a4ed - feat(data/polynomial/laurent): define `degree` and some API (#15225)

feat(data/polynomial/laurent): define `degree` and some API (#15225) This PR introduces the `degree` for Laurent polynomials. It takes values in `with_bot ℤ`and is defined as `f.support.max`. It may make sense to define a "degree" on any `add_monoid_algebra` whose value group is `linear_ordered`, but I am only defining `degree` for Laurent polynomials. The PR also proves some API lemmas about support and relationship between the degree of a Laurent polynomial and the degree with polynomials, seen as Laurent polynomials. In future PRs I intend to define also `int_degree`, analogous to `nat_degree` of polynomials.