mathlib

e18ea79e - feat(number_theory/legendre_symbol/quadratic_reciprocity): replace `[fact (p % 2 = 1)]` arguments by `(p ≠ 2)` (#13474)

feat(number_theory/legendre_symbol/quadratic_reciprocity): replace `[fact (p % 2 = 1)]` arguments by `(p ≠ 2)` (#13474) This removes implicit arguments of the form `[fact (p % 2 = 1)]` and replaces them by explicit arguments `(hp : p ≠ 2)`. (See the short discussion on April 9 in [this topic](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Quadratic.20Hilbert.20symbol.20over.20.E2.84.9A).)