mathlib
f0c8bf92 - chore(*): removed unneeded imports (#18926)

Commit
2 years ago
chore(*): removed unneeded imports (#18926) This is another run of https://github.com/leanprover-community/mathlib/pull/17568, scrubbing unnecessary imports. Like last time we only remove genuinely unneeded imports, and leave merely transitively redundant imports alone. (I *still* disagree with the objectors to removing transitively redundant imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading