mathlib

fbff76b5 - refactor(number_theory/legendre_symbol/): move Gauss/Eisenstein lemma code to separate file (#13449)

refactor(number_theory/legendre_symbol/): move Gauss/Eisenstein lemma code to separate file (#13449) In preparation of further changes to number_theory/legendre_symbol/quadratic_reciprocity, this takes most of the code dealing with the lemmas of Gauss and Eisenstein out of quadratic_reciprocity.lean into a new file gauss_eisenstein_lemmas.lean. Since I am not planning to do much (if anything) to this part of the code and it is rather involved and slows down Lean when I'm editing quadratic_reciprocity.lean, it makes sense to separate this code from the remainder of the file. Co-authored-by: Oliver Nash <github@olivernash.org>