refactor(data/{,mv_}polynomial): support function (#6615)
With polynomials, we try to avoid the function coercion in favor of the `coeff` functions. However the coercion easily leaks through the abstraction because of the `finsupp.mem_support_iff` lemma.
This PR adds the `polynomial.support` and `mv_polynomial.support` functions. This allows us to define the `polynomial.mem_support_iff` and `mv_polynomial.mem_support_iff` lemmas that are stated in terms of `coeff`.
