Commit 2022-04-18 10:31 e18ea79e
View on Github →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.)