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.





leanprover-community/mathlib,leanprover-community/mathlib