remove a partial proof

eric-wieser · Jan 7, 2024 · 0ca656c · 0ca656c
1 parent 6ccd292
commit 0ca656c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/MatrixCookbook/10FunctionsAndOperators.lean b/MatrixCookbook/10FunctionsAndOperators.lean
@@ -296,7 +296,7 @@ theorem eq_549 (A : Matrix m n ℝ) :
   ⟨A.rank_transpose.symm, A.rank_self_mul_transpose.symm, A.rank_transpose_mul_self.symm⟩
 
 theorem eq_550 (A : Matrix m m ℝ) :
-    A.PosDef ↔ ∃ B : (Matrix m m ℝ)ˣ, A = (↑B : Matrix m m ℝ) * ↑Bᵀ := by
-  rw [PosDef]
+    A.PosDef ↔ ∃ B : (Matrix m m ℝ)ˣ, A = (↑B : Matrix m m ℝ) * ↑Bᵀ :=
+  sorry
 
 end MatrixCookbook