Commit 2022-04-15 17:50 fbff76b5

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.