Commit 2022-05-16 16:38 89f2760f

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.