Commit 2022-04-22 15:16 a74df9b5

feat(number_theory/legendre_symbol): add file quadratic_char.lean (#13503) This adds the file quadratic_char.lean in number_theory/legendre_symbol/. This file contains (apart from some more general stuff on finite fields that is useful for what is done in the file) the definition of the quadratic character on a finite field F (with values in the integers) and a number of statements of properties. It also defines quadratic characters on zmod 4 and zmod 8 that will be useful for the supplements to the law of quadratic reciprocity.