mathlib

a74df9b5 - feat(number_theory/legendre_symbol): add file quadratic_char.lean (#13503)

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.