Skip to content

Commit

Permalink
Shake imports
Browse files Browse the repository at this point in the history
  • Loading branch information
@urkud
urkud committed Aug 1, 2024
1 parent 7260949 commit d2a0d35
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion SphereEversion/Indexing.lean
View file
Original file line number Diff line number Diff line change
@@ -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
/-!
Expand Down

0 comments on commit d2a0d35

Please sign in to comment.