Drop an empty file

We can recreate it later, if needed.
leanprover-community · Aug 1, 2024 · a344c1b · a344c1b
1 parent 87e3c45
commit a344c1b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git 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