matrix notation

leanprover-community · Oct 23, 2023 · 798574a · 798574a
1 parent bca61be
commit 798574a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/exercises_sources/thursday/linear_algebra.lean b/src/exercises_sources/thursday/linear_algebra.lean
@@ -133,7 +133,7 @@ Hints:
   * Use the `simp` tactic to simplify `(x + y) i` to `x i + y i` and `(s • x) i` to `s * x i`.
   * To deal with equalities containing many `+` and `*` symbols, use the `ring` tactic.
 -/
-def A : matrix (fin 2) (fin 2) R := ![![1, 0], ![-2, 1]]
+def A : matrix (fin 2) (fin 2) R := !![1, 0; -2, 1]
 def your_bilin_form : bilin_form R (fin 2 → R) :=
 sorry
 

diff --git a/src/solutions/thursday/linear_algebra.lean b/src/solutions/thursday/linear_algebra.lean
@@ -196,7 +196,7 @@ Hints:
   * Use the `simp` tactic to simplify `(x + y) i` to `x i + y i` and `(s • x) i` to `s * x i`.
   * To deal with equalities containing many `+` and `*` symbols, use the `ring` tactic.
 -/
-def A : matrix (fin 2) (fin 2) R := ![![1, 0], ![-2, 1]]
+def A : matrix (fin 2) (fin 2) R := !![1, 0; -2, 1]
 def your_bilin_form : bilin_form R (fin 2 → R) :=
 -- sorry
 { bilin := λ v w, v 0 * w 0 + v 1 * w 1 - 2 * v 1 * w 0,