Update FormalBook/Chapter_05.lean

mo271 · Nov 22, 2024 · 99449a4 · 99449a4
1 parent e7653d2
commit 99449a4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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