sorry
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)
no goals