Commit 2022-05-09 16:57 98f2779c

refactor(number_theory/legendre_symbol/*): move section general from quadratic_char.lean into new file auxiliary.lean (#14027) This is a purely administrative step (in preparation of adding more files that may need some of the auxiliary results). We move the collection of auxiliary results that constitute section general of quadratic_char.lean to a new file auxiliary.lean (and change the imports of quadratic_char.lean accordingly). This new file is meant as a temporary place for these auxiliary results; when the refactor of quadratic_reciprocity is finished, they will be moved to appropriate files in mathlib.