Tiny fix in S04_Bases.lean

Fixed an example so that it is about vector sum, not matrix sum.
avigad · Feb 3, 2025 · 343d88a · 343d88a
1 parent 024eeab
commit 343d88a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C09_Linear_Algebra/S04_Bases.lean b/MIL/C09_Linear_Algebra/S04_Bases.lean
@@ -34,7 +34,7 @@ EXAMPLES: -/
 section matrices
 
 -- Adding vectors
-#eval !![1, 2] + !![3, 4]  -- !![4, 6]
+#eval ![1, 2] + ![3, 4]  -- ![4, 6]
 
 -- Adding matrices
 #eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]