mathlib
2693ab58 - feat(number_theory/legendre_symbol): add directory legendre_symbol and move quadratic_reciprocity.lean into it (#13441)

Commit
4 years ago
feat(number_theory/legendre_symbol): add directory legendre_symbol and move quadratic_reciprocity.lean into it (#13441) In preparation of adding more code in a structured way, this sets up a new directory `legendre_symbol` below `number_theory` and moves the file `quadratic_reciprocity.lean` there. The imports in `src/number_theory/zsqrtd/gaussian_int.lean` and `archive/imo/imp2008_q3.lean` are changed accordingly.
Parents
Loading