mathlib

5b2fe805 - chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files (#19193)

chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files (#19193) The best split here is separating `quadratic_reciprocity` into that and `legendre_symbol`. I was looking at this because the olean analyser in the port-progress-bot made an unlikely claim about unnecessary dependencies, and I wanted to make sure we weren't missing something in doubting it. We weren't. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>