mathlib

89f2760f - feat(number_theory/legendre_symbol/*): move characters on `zmod n` to new file, add API, improve a proof (#14178)

feat(number_theory/legendre_symbol/*): move characters on `zmod n` to new file, add API, improve a proof (#14178) This is another "administrative" PR with the goal to have a better file structure. It moves the section `quad_char_mod_p` from `quadratic_char.lean` to a new file `zmod_char.lean`. It also adds some API lemmas for `χ₈` and `χ₈'` (which will be useful when dealing with the value of quadratic characters at 2 and -2), and I have used the opportunity to shorten the proof of `χ₄_eq_neg_one_pow`.