refactor(algebra/squarefree): split out nat part to new file `data/…

…nat/squarefree` (#14577) As discussed in this Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/squarefree.2C.20is_prime_pow.2C.20and.20factorization)
leanprover-community · Jun 7, 2022 · 6906627 · 6906627
1 parent 4a4cd6d
commit 6906627
Show file tree

Hide file tree

Showing 5 changed files with 534 additions and 515 deletions.
diff --git a/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean b/archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
 import topology.instances.ennreal
-import algebra.squarefree
+import data.nat.squarefree
 
 /-!
 # Divergence of the Prime Reciprocal Series