From 7bd7d0bce88e078bc69acf728360fb4aa0bb29f8 Mon Sep 17 00:00:00 2001
From: yhtq <1414672068@qq.com>
Date: Sat, 26 Oct 2024 14:07:58 +0800
Subject: [PATCH] change dir

---
 .gitignore                                                | 1 +
 {Others => ModuleLocalProperties}/restrictScalarsHom.lean | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)
 rename {Others => ModuleLocalProperties}/restrictScalarsHom.lean (96%)

diff --git a/.gitignore b/.gitignore
index bfb30ec..b9995ce 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /.lake
+Others/** 
\ No newline at end of file
diff --git a/Others/restrictScalarsHom.lean b/ModuleLocalProperties/restrictScalarsHom.lean
similarity index 96%
rename from Others/restrictScalarsHom.lean
rename to ModuleLocalProperties/restrictScalarsHom.lean
index 4d5f14b..2fcdfd2 100644
--- a/Others/restrictScalarsHom.lean
+++ b/ModuleLocalProperties/restrictScalarsHom.lean
@@ -181,5 +181,6 @@ noncomputable def aut_equiv_of_finrank_eq_one {F S A : Type*}
     intro x
     apply AlgEquiv.ext
     intro y
-    simp?  [AlgEquiv.restrictScalarsHom, AlgEquiv.restrictScalars]
+    simp only [AlgEquiv.restrictScalarsHom, AlgEquiv.restrictScalars, RingEquiv.toEquiv_eq_coe,
+      MonoidHom.coe_mk, OneHom.coe_mk, AlgEquiv.coe_mk, EquivLike.coe_coe, AlgEquiv.coe_ringEquiv]
   map_mul' := (AlgEquiv.restrictScalarsHom F S A).map_mul'