change dir

mbkybky · Oct 26, 2024 · 7bd7d0b · 7bd7d0b
1 parent f3cf378
commit 7bd7d0b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/.gitignore b/.gitignore
@@ -1 +1,2 @@
 /.lake
+Others/** 
diff --git a/Others/restrictScalarsHom.lean → ...leLocalProperties/restrictScalarsHom.lean b/Others/restrictScalarsHom.lean → ...leLocalProperties/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'