From 99449a41a90ac57fa33d25d08df3f0a44e5dedcc Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 22 Nov 2024 08:24:39 +0100
Subject: [PATCH] Update FormalBook/Chapter_05.lean

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

diff --git a/FormalBook/Chapter_05.lean b/FormalBook/Chapter_05.lean
index 23f3442..8403fcf 100644
--- a/FormalBook/Chapter_05.lean
+++ b/FormalBook/Chapter_05.lean
@@ -114,7 +114,7 @@ lemma fact_B (p : ℕ) [Fact (Prime p)] (K : Type _) [Field K] (ζ : Kˣ) (h_1 :
 theorem quadratic_reciprocity_2 (p q : ℕ) (hp : p ≠ 2) (hq : q ≠ 2)
   [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] :
   (legendre_sym p q) * (legendre_sym q p) = -1 ^ ((p-1) / 2 * (q - 1) / 2 ) := by
-  exact book.quadratic_reciprocity.quadratic_reciprocity_1 p q hp hq
+  sorry
 
 
 end quadratic_reciprocity