mathlib

249fd4f2 - refactor(data/polynomial,ring_theory): use big operators for polynomials (#6616)

refactor(data/polynomial,ring_theory): use big operators for polynomials (#6616) This untangles some more definitions on polynomials from finsupp. This uses the same approach as in #6605.