mathlib
93468fee - chore(algebraic_geometry/Spec): reduce imports (#4007)

Commit
5 years ago
chore(algebraic_geometry/Spec): reduce imports (#4007) The main change is to remove some `example`s from `topology.category.TopCommRing`, so that we don't need to know about the real and complex numbers on the way to defining a `Scheme`. While I was staring at `leanproject import-graph --to algebraic_geometry.Scheme`, I also removed a bunch of redundant or unused imports elsewhere. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading