add one lemma

eric-wieser · Jan 6, 2024 · 37dec65 · 37dec65
1 parent 0f41cd8
commit 37dec65
Showing 1 changed file with 8 additions and 3 deletions.
diff --git a/MatrixCookbook/9SpecialMatrices.lean b/MatrixCookbook/9SpecialMatrices.lean
@@ -299,9 +299,14 @@ theorem eq442 : sorry :=
 
 /-! ### Definition -/
 
-
-theorem eq443 : sorry :=
-  sorry
+-- note this is 0-indexed not 1-indexed
+theorem eq443 :
+    stdBasisMatrix (1 : Fin 4) (2 : Fin 4) 1 =
+      !![0, 0, 0, 0;
+         0, 0, 1, 0;
+         0, 0, 0, 0;
+         0, 0, 0, 0] := by
+  decide
 
 /-! ### Swap and Zeros -/