From 03bffeceaef98403d74922bffdd3f2d936890c55 Mon Sep 17 00:00:00 2001
From: Heath Sanchez <heath@intaface.io>
Date: Mon, 6 Jul 2026 12:39:19 +1200
Subject: [PATCH] Fill polynomial evaluation norm step in Chapter 06

---
 FormalBook/Chapter_06.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean
index 069ed2f..dfb0ab4 100644
--- a/FormalBook/Chapter_06.lean
+++ b/FormalBook/Chapter_06.lean
@@ -75,7 +75,7 @@ theorem h_lamb_gt_q_sub_one (q n : ℕ) (lamb : ℂ):
   have h_ineq :
       ‖((X - C lamb).eval (q : ℂ))‖^2 > ((q : ℝ) - 1)^2  := by
     calc
-      _ = ‖q - lamb‖^2 := by sorry
+      _ = ‖q - lamb‖^2 := by simp
         --simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
       _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
       _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry