Drop ToMathlib/Data/Set/Prod

It contained 1 lemma provable by `simp`
leanprover-community · Aug 1, 2024 · 9b57282 · 9b57282
1 parent 62ac547
commit 9b57282
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 11 deletions.
diff --git a/SphereEversion.lean b/SphereEversion.lean
@@ -41,7 +41,6 @@ import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
 import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm
 import SphereEversion.ToMathlib.Data.Nat.Basic
 import SphereEversion.ToMathlib.Data.Set.Lattice
-import SphereEversion.ToMathlib.Data.Set.Prod
 import SphereEversion.ToMathlib.Equivariant
 import SphereEversion.ToMathlib.ExistsOfConvex
 import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm

diff --git a/SphereEversion/ToMathlib/Data/Set/Prod.lean b/SphereEversion/ToMathlib/Data/Set/Prod.lean