Commit 2020-07-17 13:47 89996255
View on Github →chore(*): more import reduction (#3421)
Another import reduction PR. (This is by hand, not just removing transitive imports.)
Mostly this one is from staring at leanproject import-graph --to data.polynomial.basic and wondering about weird edges in the graph.