From 1142bfe021aecde97fe6465e1c064fdf009ee84b Mon Sep 17 00:00:00 2001 From: FM22 Date: Wed, 8 Jan 2025 01:47:58 +0000 Subject: [PATCH] fix --- RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean b/RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean index 0904aa3..6d69801 100644 --- 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