mathlib
64e464f1 - chore(*): remove unnecessary transitive imports (#2496)

Commit
5 years ago
chore(*): remove unnecessary transitive imports (#2496) This removes all imports which have already been imported by other imports. Overall, this is slightly over a third of the total import lines. This should have no effect whatsoever on compilation, but should make `leanproject import-graph` somewhat... leaner! Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Keeley Hoek <keeley@hoek.io>
Author
Parents
Loading