mathlib

1627d8d7 - feat(number_theory/legendre_symbol/*): redefine quadratic characters as `mul_char`s (#15418)

feat(number_theory/legendre_symbol/*): redefine quadratic characters as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).