fix

artie2000 · Jan 8, 2025 · 1142bfe · 1142bfe
1 parent 9b34723
commit 1142bfe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean b/RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Florent Schaffhauser, Artie Khovanov
 -/
-import Mathlib.Algebra.Ring.SumsOfSquares
+import RealClosedField.Mathlib.Algebra.Ring.SumsOfSquares
 
 /-!
 # Semireal rings