From d2a0d3557cb7ec297c0b560bd69ce86dd766c692 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 1 Aug 2024 14:52:11 -0400
Subject: [PATCH] Shake imports

---
 SphereEversion/Indexing.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean
index dc44dfe7..b4079f02 100644
--- a/SphereEversion/Indexing.lean
+++ b/SphereEversion/Indexing.lean
@@ -1,7 +1,6 @@
 import Mathlib.Order.Interval.Finset.Fin
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Nat.SuccPred
-import Mathlib.Data.ZMod.Defs
 import Mathlib.SetTheory.Cardinal.Basic
 import SphereEversion.ToMathlib.Data.Nat.Basic
 /-!