chore(*): move quadratic_reciprocity to number_theory/ (#2520)

I've never really understood why we put all these cool theorems under the data/ directory, so I suggest moving them out of there, and into the place where thy "belong".
leanprover-community · Apr 25, 2020 · f192f2f · f192f2f
1 parent 3c8584d
commit f192f2f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/src/data/zsqrtd/gaussian_int.lean b/src/data/zsqrtd/gaussian_int.lean
@@ -6,7 +6,7 @@ Author: Chris Hughes
 import data.zsqrtd.basic
 import data.complex.basic
 import ring_theory.principal_ideal_domain
-import data.zmod.quadratic_reciprocity
+import number_theory.quadratic_reciprocity
 /-!
 # Gaussian integers
 

diff --git a/src/data/zmod/quadratic_reciprocity.lean → src/number_theory/quadratic_reciprocity.lean b/src/data/zmod/quadratic_reciprocity.lean → src/number_theory/quadratic_reciprocity.lean