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

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a b : ℤ
⊢ legendre_sym p (a * b) = legendre_sym p a * legendre_sym p b
Tactic:
sorry
State after:
no goals