diff --git a/SphereEversion.lean b/SphereEversion.lean index 1419c40e..dfa89056 100644 --- a/SphereEversion.lean +++ b/SphereEversion.lean @@ -60,7 +60,6 @@ import SphereEversion.ToMathlib.Order.Filter.Basic import SphereEversion.ToMathlib.Partition import SphereEversion.ToMathlib.SmoothBarycentric import SphereEversion.ToMathlib.Topology.Algebra.Module -import SphereEversion.ToMathlib.Topology.Germ import SphereEversion.ToMathlib.Topology.HausdorffDistance import SphereEversion.ToMathlib.Topology.Misc import SphereEversion.ToMathlib.Topology.Paracompact diff --git a/SphereEversion/ToMathlib/Topology/Germ.lean b/SphereEversion/ToMathlib/Topology/Germ.lean deleted file mode 100644 index a02e2ec7..00000000 --- a/SphereEversion/ToMathlib/Topology/Germ.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Mathlib.Topology.Germ --- leaving this file blank, for future PRs moving material here