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.
