doc

staroperator · staroperator · commit a7972c9e0d95 · 2025-11-28T22:47:40.000-05:00
diff --git a/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean b/Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean
@@ -17,8 +17,9 @@ import Mathlib.LinearAlgebra.Matrix.Notation
 /-!
 # Presburger definability and semilinear sets
 
-This file formalizes the equivalence between Presburger definable sets and semilinear sets. As an
-application of this result, we show that the graph of multiplication is not Presburger definable.
+This file formalizes the classical result that Presburger definable sets are the same as semilinear
+sets. As an application of this result, we show that the graph of multiplication is not Presburger
+definable.
 
 ## Main Results
 
