Commit 2021-03-11 17:09 95a8e958

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.