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

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
⊢ ↑a ≠ 0 → ↑(legendre_sym p a) = ↑a ^ ((p - 1) / 2)
Tactic:
sorry
State after:
no goals