): remove unnecessary imports (#8578)

Commit

4 years ago

chore(algebra/*, data/polynomial/*): remove unnecessary imports (#8578) I cleaned up all of `data.polynomial`, and the files in `algebra` it imports.

Author

YaelDillies

Parents

mathlib3 3788cbfa - chore(algebra/*, data/polynomial/*): remove unnecessary imports (#8578)