先进行第14节课，三阶魔方相关定理的证明

chenjulang · Jan 11, 2024 · e03283e · e03283e
1 parent 797f16c
commit e03283e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/LeanCourse/Video/Learning8_test4.lean b/LeanCourse/Video/Learning8_test4.lean
@@ -128,7 +128,8 @@ variable {n p} [Fintype n] [Fintype p]
         rw [
         ← List.take_length (listTransvecRow2 M),
         A]
-        refine' mul_listTransvecRow_last_col_take M i _ -- 实际上更核心的应该是mul_listTransvecRow_last_col_take
+        refine' mul_listTransvecRow_last_col_take M i _
+        -- 实际上更核心的应该是mul_listTransvecRow_last_col_take，用归纳法证明的
         simp only [le_refl]
         done