Commit 2022-06-12 16:53 d6eb634b

feat(number_theory/legendre_symbol/auxiliary, *): add/move lemmas in/to various files, delete auxiliary.lean (#14572) This is the first PR in a series that will culminate in providing the proof of Quadratic Reciprocity using Gauss sums. Here we just add some lemmas to the file auxiliary.lean that will be used in new code later. We also generalize the lemmas neg_one_ne_one_of_char_ne_two and neg_ne_self_of_char_ne_two from finite fields to more general rings. See this Zulipt topic for more information. CHANGE OF PLAN: Following the discussion on Zulip linked to above, the lemmas in auxiliary.lean are supposed to be moved to there proper places. I have added suggestions to each lemma or group of lemmas (or definitions) what the proper place could be (in some cases, there are alternatives). Please comment if you do not agree or to support one of the alternatives.