Use repository imports in conjecture statements

google-deepmind · Paul-Lez · Aug 19, 2026 · Aug 19, 2026 · Aug 19, 2026 · Aug 19, 2026
commit e329be48af2ae7bdd722832ea33e7bb322239e94
diff --git a/FormalConjectures/Other/CaratheodoryConjecture.lean b/FormalConjectures/Other/CaratheodoryConjecture.lean
@@ -14,9 +14,8 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import Mathlib.Analysis.Convex.Body
-import FormalConjectures.Other.LoewnerConjecture
 import FormalConjecturesUtil
+import FormalConjectures.Other.LoewnerConjecture
 
 /-!
 # Carathéodory's conjecture

diff --git a/FormalConjectures/Other/LoewnerConjecture.lean b/FormalConjectures/Other/LoewnerConjecture.lean
@@ -14,7 +14,6 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import Mathlib.Analysis.Normed.Module.Normalize
 import FormalConjecturesUtil
 
 /-!
-Original file line number
+Diff line change
@@ Expand Up @@
     limitations under the License.
     -/
-    import Mathlib.Analysis.Normed.Module.Normalize
     import FormalConjecturesUtil
     /-!
@@ Expand Down @@