Commit 2022-05-03 18:19 bd1d9359

feat(number_theory/legendre_symbol/): add some lemmas (#13831) This adds essentially two lemmas on quadratic characters:

• quadratic_char_neg_one_iff_not_is_square, which says that the quadratic character takes the value -1 exactly on non-squares, and
• quadratic_char_number_of_sqrts. which says that the number of square roots of a : F is quadratic_char F a + 1. It also adds the corresponding statements, legendre_sym_eq_neg_one_iff and legendre_sym_number_of_sqrts, for the Legendre symbol.