chore(data/finsupp/ne_locus): reduce import, after the finsupp.basic …

…refactor (#16165) Importing `data.finsupp.defs` is enough.
leanprover-community · Aug 20, 2022 · 2c6e595 · 2c6e595
1 parent 21b6412
commit 2c6e595
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/finsupp/ne_locus.lean b/src/data/finsupp/ne_locus.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.finsupp.basic
+import data.finsupp.defs
 
 /-!
 # Locus of unequal values of finitely supported functions