mathlib3

9d74f9b0 - chore(data/polynomial): reduce imports (#3419)

chore(data/polynomial): reduce imports (#3419) Now that @jalex-stark has split up `data.polynomial` into submodules, this PR minimises imports. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>