mathlib3

d6eb634b - feat(number_theory/legendre_symbol/auxiliary, *): add/move lemmas in/to various files, delete `auxiliary.lean` (#14572)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Quadratic.20Hilbert.20symbol.20over.20.E2.84.9A/near/285053214) 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.