mathlib

eea16dc8 - feat(number_theory/legendre_symbol/*): add results on value at -1 (#13978)

feat(number_theory/legendre_symbol/*): add results on value at -1 (#13978) This PR adds code expressing the value of the quadratic character at -1 of a finite field of odd characteristic as χ₄ applied to the cardinality of the field. This is then also done for the Legendre symbol. Additional changes: * two helper lemmas `odd_mod_four` and `finite_field.even_card_of_char_two` that are needed * some API lemmas for χ₄ * write `euler_criterion` and `exists_sq_eq_neg_one_iff` in terms of `is_square`; simplify the proof of the latter using the general result for quadratic characters