Commit 2022-07-18 12:17 1627d8d7

feat(number_theory/legendre_symbol/*): redefine quadratic characters as mul_chars (#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.