Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-22 16:17 591a0a00

View on Github →

chore(*): only import one file per line (#2470) This perhaps-unnecessarily-obsessive PR puts every import statement on its own line. Why?

  1. it's nice to be able to grep for import X
  2. if we enforced this, it would be easier deal with commands after imports, etc. (irrelevant in 3.9)
  3. it means I can remove all unnecessary transitive imports with a script
  4. it's just tidier. :-)

Estimated changes