We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 1ddc48d commit 1ec83c5Copy full SHA for 1ec83c5
1 file changed
Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean
@@ -13,8 +13,8 @@ import Mathlib.Data.Matrix.ColumnRowPartitioned
13
import Mathlib.Data.Pi.Interval
14
import Mathlib.Data.Rat.Floor
15
import Mathlib.LinearAlgebra.Matrix.ToLin
16
-import Mathlib.ModelTheory.Definability
17
import Mathlib.ModelTheory.Arithmetic.Presburger.Basic
+import Mathlib.ModelTheory.Definability
18
import Mathlib.RingTheory.Localization.Module
19
20
/-!
0 commit comments