Shake imports

leanprover-community · Oct 28, 2024 · 932ddf0 · 932ddf0
1 parent dde5e3c
commit 932ddf0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.Data.Fin.Tuple.Basic
-import Mathlib.Data.List.Range
+import Mathlib.Data.List.Defs
 
 /-!
 # Matrix and vector notation