update

staroperator · staroperator · commit 38fd9621da60 · 2025-11-28T22:47:40.000-05:00
diff --git a/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean b/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean
@@ -6,7 +6,7 @@ Authors: Dexin Zhang
 import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.ModelTheory.Arithmetic.Presburger.Basic
-import Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.FinitelyGenerated
+import Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
 import Mathlib.ModelTheory.Definability
 
 /-!
