Theorem: book.quadratic_reciprocity.quadratic_reciprocity_2 (FormalBook/Chapter_05.lean)

State before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝² : Fact p✝.Prime
p q : ℕ
hp : p ≠ 2
hq : q ≠ 2
inst✝¹ : Fact p.Prime
inst✝ : Fact q.Prime
⊢ legendre_sym p ↑q * legendre_sym q ↑p = -1 ^ ((p - 1) / 2 * (q - 1) / 2)
Tactic:
sorry
State after:
no goals