2022-04-26 17:50
src/number_theory/legendre_symbol/quadratic_char.lean
refactor(number_theory/legendre_symbol/quadratic_reciprocity.lean): change definition of legendre_sym, simplify proofs, add lemmas (#13667) …
Deleted finite_field.unit_is_sqare_iff