Commit 2022-05-06 18:45 eea16dc8

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