From 700181a31a17a8f4236ab93a1cd0115e89eee369 Mon Sep 17 00:00:00 2001
From: Stuart Presnell <stuart.presnell@gmail.com>
Date: Wed, 8 Jun 2022 13:42:38 +0000
Subject: [PATCH] refactor(algebra/is_prime_pow): move lemmas using
 `factorization` to new file (#14598)

As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/squarefree.2C.20is_prime_pow.2C.20and.20factorization/near/285144241).
---
 src/algebra/is_prime_pow.lean                 | 124 ----------------
 .../basic.lean}                               |   0
 src/data/nat/factorization/prime_pow.lean     | 138 ++++++++++++++++++
 src/data/nat/squarefree.lean                  |   2 +-
 src/field_theory/cardinality.lean             |   1 +
 src/group_theory/nilpotent.lean               |   2 +-
 src/group_theory/sylow.lean                   |   2 +-
 src/number_theory/arithmetic_function.lean    |   2 +-
 src/number_theory/padics/padic_val.lean       |   2 +-
 src/ring_theory/multiplicity.lean             |   2 +-
 10 files changed, 145 insertions(+), 130 deletions(-)
 rename src/data/nat/{factorization.lean => factorization/basic.lean} (100%)
 create mode 100644 src/data/nat/factorization/prime_pow.lean

diff --git a/src/algebra/is_prime_pow.lean b/src/algebra/is_prime_pow.lean
index 73a651a3d1a76..6b57ede3c6afd 100644
--- a/src/algebra/is_prime_pow.lean
+++ b/src/algebra/is_prime_pow.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import algebra.associated
-import data.nat.factorization
 import number_theory.divisors
 
 /-!
@@ -96,30 +95,6 @@ end
 instance {n : ℕ} : decidable (is_prime_pow n) :=
 decidable_of_iff' _ (is_prime_pow_nat_iff_bounded n)
 
-lemma is_prime_pow.min_fac_pow_factorization_eq {n : ℕ} (hn : is_prime_pow n) :
-  n.min_fac ^ n.factorization n.min_fac = n :=
-begin
-  obtain ⟨p, k, hp, hk, rfl⟩ := hn,
-  rw ←nat.prime_iff at hp,
-  rw [hp.pow_min_fac hk.ne', hp.factorization_pow, finsupp.single_eq_same],
-end
-
-lemma is_prime_pow_of_min_fac_pow_factorization_eq {n : ℕ}
-  (h : n.min_fac ^ n.factorization n.min_fac = n) (hn : n ≠ 1) :
-  is_prime_pow n :=
-begin
-  rcases eq_or_ne n 0 with rfl | hn',
-  { simpa using h },
-  refine ⟨_, _, nat.prime_iff.1 (nat.min_fac_prime hn), _, h⟩,
-  rw [pos_iff_ne_zero, ←finsupp.mem_support_iff, nat.factor_iff_mem_factorization,
-    nat.mem_factors_iff_dvd hn' (nat.min_fac_prime hn)],
-  apply nat.min_fac_dvd
-end
-
-lemma is_prime_pow_iff_min_fac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :
-  is_prime_pow n ↔ n.min_fac ^ n.factorization n.min_fac = n :=
-⟨λ h, h.min_fac_pow_factorization_eq, λ h, is_prime_pow_of_min_fac_pow_factorization_eq h hn⟩
-
 lemma is_prime_pow.dvd {n m : ℕ} (hn : is_prime_pow n) (hm : m ∣ n) (hm₁ : m ≠ 1) :
   is_prime_pow m :=
 begin
@@ -132,90 +107,6 @@ begin
   simpa using hm₁,
 end
 
-lemma is_prime_pow_iff_factorization_eq_single {n : ℕ} :
-  is_prime_pow n ↔ ∃ p k : ℕ, 0 < k ∧ n.factorization = finsupp.single p k :=
-begin
-  rw is_prime_pow_nat_iff,
-  refine exists₂_congr (λ p k, _),
-  split,
-  { rintros ⟨hp, hk, hn⟩,
-    exact ⟨hk, by rw [←hn, nat.prime.factorization_pow hp]⟩ },
-  { rintros ⟨hk, hn⟩,
-    have hn0 : n ≠ 0,
-    { rintro rfl,
-      simpa only [finsupp.single_eq_zero, eq_comm, nat.factorization_zero, hk.ne'] using hn },
-    rw nat.eq_pow_of_factorization_eq_single hn0 hn,
-    exact ⟨nat.prime_of_mem_factorization
-      (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩ }
-end
-
-lemma is_prime_pow_iff_card_support_factorization_eq_one {n : ℕ} :
-  is_prime_pow n ↔ n.factorization.support.card = 1 :=
-by simp_rw [is_prime_pow_iff_factorization_eq_single, finsupp.card_support_eq_one', exists_prop,
-  pos_iff_ne_zero]
-
-/-- An equivalent definition for prime powers: `n` is a prime power iff there is a unique prime
-dividing it. -/
-lemma is_prime_pow_iff_unique_prime_dvd {n : ℕ} :
-  is_prime_pow n ↔ ∃! p : ℕ, p.prime ∧ p ∣ n :=
-begin
-  rw is_prime_pow_nat_iff,
-  split,
-  { rintro ⟨p, k, hp, hk, rfl⟩,
-    refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, _⟩,
-    rintro q ⟨hq, hq'⟩,
-    exact (nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq') },
-  rintro ⟨p, ⟨hp, hn⟩, hq⟩,
-  -- Take care of the n = 0 case
-  rcases eq_or_ne n 0 with rfl | hn₀,
-  { obtain ⟨q, hq', hq''⟩ := nat.exists_infinite_primes (p + 1),
-    cases hq q ⟨hq'', by simp⟩,
-    simpa using hq' },
-  -- So assume 0 < n
-  refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, _⟩,
-  simp only [and_imp] at hq,
-  apply nat.dvd_antisymm (nat.pow_factorization_dvd _ _),
-  -- We need to show n ∣ p ^ n.factorization p
-  apply nat.dvd_of_factors_subperm hn₀,
-  rw [hp.factors_pow, list.subperm_ext_iff],
-  intros q hq',
-  rw nat.mem_factors hn₀ at hq',
-  cases hq _ hq'.1 hq'.2,
-  simp,
-end
-
-lemma is_prime_pow_pow_iff {n k : ℕ} (hk : k ≠ 0) :
-  is_prime_pow (n ^ k) ↔ is_prime_pow n :=
-begin
-  simp only [is_prime_pow_iff_unique_prime_dvd],
-  apply exists_unique_congr,
-  simp only [and.congr_right_iff],
-  intros p hp,
-  exact ⟨hp.dvd_of_dvd_pow, λ t, t.trans (dvd_pow_self _ hk)⟩,
-end
-
-lemma nat.coprime.is_prime_pow_dvd_mul {n a b : ℕ} (hab : nat.coprime a b) (hn : is_prime_pow n) :
-  n ∣ a * b ↔ n ∣ a ∨ n ∣ b :=
-begin
-  rcases eq_or_ne a 0 with rfl | ha,
-  { simp only [nat.coprime_zero_left] at hab,
-    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
-  rcases eq_or_ne b 0 with rfl | hb,
-  { simp only [nat.coprime_zero_right] at hab,
-    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
-  refine ⟨_, λ h, or.elim h (λ i, i.trans (dvd_mul_right _ _)) (λ i, i.trans (dvd_mul_left _ _))⟩,
-  obtain ⟨p, k, hp, hk, rfl⟩ := (is_prime_pow_nat_iff _).1 hn,
-  simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb),
-    nat.factorization_mul ha hb, hp.pow_dvd_iff_le_factorization ha,
-    hp.pow_dvd_iff_le_factorization hb, pi.add_apply, finsupp.coe_add],
-  have : a.factorization p = 0 ∨ b.factorization p = 0,
-  { rw [←finsupp.not_mem_support_iff, ←finsupp.not_mem_support_iff, ←not_and_distrib,
-      ←finset.mem_inter],
-    exact λ t, nat.factorization_disjoint_of_coprime hab t },
-  cases this;
-  simp [this, imp_or_distrib],
-end
-
 lemma nat.disjoint_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :
   disjoint (a.divisors.filter is_prime_pow) (b.divisors.filter is_prime_pow) :=
 begin
@@ -224,21 +115,6 @@ begin
   exact hn.ne_one (nat.eq_one_of_dvd_coprimes hab han hbn),
 end
 
-lemma nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :
-  (a * b).divisors.filter is_prime_pow = (a.divisors ∪ b.divisors).filter is_prime_pow :=
-begin
-  rcases eq_or_ne a 0 with rfl | ha,
-  { simp only [nat.coprime_zero_left] at hab,
-    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
-  rcases eq_or_ne b 0 with rfl | hb,
-  { simp only [nat.coprime_zero_right] at hab,
-    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
-  ext n,
-  simp only [ha, hb, finset.mem_union, finset.mem_filter, nat.mul_eq_zero, and_true, ne.def,
-    and.congr_left_iff, not_false_iff, nat.mem_divisors, or_self],
-  apply hab.is_prime_pow_dvd_mul,
-end
-
 lemma is_prime_pow.two_le : ∀ {n : ℕ}, is_prime_pow n → 2 ≤ n
 | 0 h := (not_is_prime_pow_zero h).elim
 | 1 h := (not_is_prime_pow_one h).elim
diff --git a/src/data/nat/factorization.lean b/src/data/nat/factorization/basic.lean
similarity index 100%
rename from src/data/nat/factorization.lean
rename to src/data/nat/factorization/basic.lean
diff --git a/src/data/nat/factorization/prime_pow.lean b/src/data/nat/factorization/prime_pow.lean
new file mode 100644
index 0000000000000..106daf224ff01
--- /dev/null
+++ b/src/data/nat/factorization/prime_pow.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2022 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import algebra.is_prime_pow
+import data.nat.factorization.basic
+
+/-!
+# Prime powers and factorizations
+
+This file deals with factorizations of prime powers.
+-/
+
+variables {R : Type*} [comm_monoid_with_zero R] (n p : R) (k : ℕ)
+
+lemma is_prime_pow.min_fac_pow_factorization_eq {n : ℕ} (hn : is_prime_pow n) :
+  n.min_fac ^ n.factorization n.min_fac = n :=
+begin
+  obtain ⟨p, k, hp, hk, rfl⟩ := hn,
+  rw ←nat.prime_iff at hp,
+  rw [hp.pow_min_fac hk.ne', hp.factorization_pow, finsupp.single_eq_same],
+end
+
+lemma is_prime_pow_of_min_fac_pow_factorization_eq {n : ℕ}
+  (h : n.min_fac ^ n.factorization n.min_fac = n) (hn : n ≠ 1) :
+  is_prime_pow n :=
+begin
+  rcases eq_or_ne n 0 with rfl | hn',
+  { simpa using h },
+  refine ⟨_, _, nat.prime_iff.1 (nat.min_fac_prime hn), _, h⟩,
+  rw [pos_iff_ne_zero, ←finsupp.mem_support_iff, nat.factor_iff_mem_factorization,
+    nat.mem_factors_iff_dvd hn' (nat.min_fac_prime hn)],
+  apply nat.min_fac_dvd
+end
+
+lemma is_prime_pow_iff_min_fac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :
+  is_prime_pow n ↔ n.min_fac ^ n.factorization n.min_fac = n :=
+⟨λ h, h.min_fac_pow_factorization_eq, λ h, is_prime_pow_of_min_fac_pow_factorization_eq h hn⟩
+
+lemma is_prime_pow_iff_factorization_eq_single {n : ℕ} :
+  is_prime_pow n ↔ ∃ p k : ℕ, 0 < k ∧ n.factorization = finsupp.single p k :=
+begin
+  rw is_prime_pow_nat_iff,
+  refine exists₂_congr (λ p k, _),
+  split,
+  { rintros ⟨hp, hk, hn⟩,
+    exact ⟨hk, by rw [←hn, nat.prime.factorization_pow hp]⟩ },
+  { rintros ⟨hk, hn⟩,
+    have hn0 : n ≠ 0,
+    { rintro rfl,
+      simpa only [finsupp.single_eq_zero, eq_comm, nat.factorization_zero, hk.ne'] using hn },
+    rw nat.eq_pow_of_factorization_eq_single hn0 hn,
+    exact ⟨nat.prime_of_mem_factorization
+      (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩ }
+end
+
+lemma is_prime_pow_iff_card_support_factorization_eq_one {n : ℕ} :
+  is_prime_pow n ↔ n.factorization.support.card = 1 :=
+by simp_rw [is_prime_pow_iff_factorization_eq_single, finsupp.card_support_eq_one', exists_prop,
+  pos_iff_ne_zero]
+
+/-- An equivalent definition for prime powers: `n` is a prime power iff there is a unique prime
+dividing it. -/
+lemma is_prime_pow_iff_unique_prime_dvd {n : ℕ} :
+  is_prime_pow n ↔ ∃! p : ℕ, p.prime ∧ p ∣ n :=
+begin
+  rw is_prime_pow_nat_iff,
+  split,
+  { rintro ⟨p, k, hp, hk, rfl⟩,
+    refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, _⟩,
+    rintro q ⟨hq, hq'⟩,
+    exact (nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq') },
+  rintro ⟨p, ⟨hp, hn⟩, hq⟩,
+  -- Take care of the n = 0 case
+  rcases eq_or_ne n 0 with rfl | hn₀,
+  { obtain ⟨q, hq', hq''⟩ := nat.exists_infinite_primes (p + 1),
+    cases hq q ⟨hq'', by simp⟩,
+    simpa using hq' },
+  -- So assume 0 < n
+  refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, _⟩,
+  simp only [and_imp] at hq,
+  apply nat.dvd_antisymm (nat.pow_factorization_dvd _ _),
+  -- We need to show n ∣ p ^ n.factorization p
+  apply nat.dvd_of_factors_subperm hn₀,
+  rw [hp.factors_pow, list.subperm_ext_iff],
+  intros q hq',
+  rw nat.mem_factors hn₀ at hq',
+  cases hq _ hq'.1 hq'.2,
+  simp,
+end
+
+lemma is_prime_pow_pow_iff {n k : ℕ} (hk : k ≠ 0) :
+  is_prime_pow (n ^ k) ↔ is_prime_pow n :=
+begin
+  simp only [is_prime_pow_iff_unique_prime_dvd],
+  apply exists_unique_congr,
+  simp only [and.congr_right_iff],
+  intros p hp,
+  exact ⟨hp.dvd_of_dvd_pow, λ t, t.trans (dvd_pow_self _ hk)⟩,
+end
+
+lemma nat.coprime.is_prime_pow_dvd_mul {n a b : ℕ} (hab : nat.coprime a b) (hn : is_prime_pow n) :
+  n ∣ a * b ↔ n ∣ a ∨ n ∣ b :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { simp only [nat.coprime_zero_left] at hab,
+    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
+  rcases eq_or_ne b 0 with rfl | hb,
+  { simp only [nat.coprime_zero_right] at hab,
+    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
+  refine ⟨_, λ h, or.elim h (λ i, i.trans (dvd_mul_right _ _)) (λ i, i.trans (dvd_mul_left _ _))⟩,
+  obtain ⟨p, k, hp, hk, rfl⟩ := (is_prime_pow_nat_iff _).1 hn,
+  simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb),
+    nat.factorization_mul ha hb, hp.pow_dvd_iff_le_factorization ha,
+    hp.pow_dvd_iff_le_factorization hb, pi.add_apply, finsupp.coe_add],
+  have : a.factorization p = 0 ∨ b.factorization p = 0,
+  { rw [←finsupp.not_mem_support_iff, ←finsupp.not_mem_support_iff, ←not_and_distrib,
+      ←finset.mem_inter],
+    exact λ t, nat.factorization_disjoint_of_coprime hab t },
+  cases this;
+  simp [this, imp_or_distrib],
+end
+
+lemma nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :
+  (a * b).divisors.filter is_prime_pow = (a.divisors ∪ b.divisors).filter is_prime_pow :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { simp only [nat.coprime_zero_left] at hab,
+    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
+  rcases eq_or_ne b 0 with rfl | hb,
+  { simp only [nat.coprime_zero_right] at hab,
+    simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
+  ext n,
+  simp only [ha, hb, finset.mem_union, finset.mem_filter, nat.mul_eq_zero, and_true, ne.def,
+    and.congr_left_iff, not_false_iff, nat.mem_divisors, or_self],
+  apply hab.is_prime_pow_dvd_mul,
+end
diff --git a/src/data/nat/squarefree.lean b/src/data/nat/squarefree.lean
index b19c12f59ab05..fb981dcd2e8ca 100644
--- a/src/data/nat/squarefree.lean
+++ b/src/data/nat/squarefree.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import ring_theory.int.basic
-import algebra.is_prime_pow
+import data.nat.factorization.prime_pow
 import algebra.squarefree
 
 /-!
diff --git a/src/field_theory/cardinality.lean b/src/field_theory/cardinality.lean
index b4f64410e6327..8d854bc69e0d0 100644
--- a/src/field_theory/cardinality.lean
+++ b/src/field_theory/cardinality.lean
@@ -10,6 +10,7 @@ import field_theory.finite.galois_field
 import logic.equiv.transfer_instance
 import ring_theory.localization.cardinality
 import set_theory.cardinal.divisibility
+import data.nat.factorization.prime_pow
 
 /-!
 # Cardinality of Fields
diff --git a/src/group_theory/nilpotent.lean b/src/group_theory/nilpotent.lean
index 77c70116bfa64..53ed68c0d2a8d 100644
--- a/src/group_theory/nilpotent.lean
+++ b/src/group_theory/nilpotent.lean
@@ -8,7 +8,7 @@ import group_theory.quotient_group
 import group_theory.solvable
 import group_theory.p_group
 import group_theory.sylow
-import data.nat.factorization
+import data.nat.factorization.basic
 import tactic.tfae
 
 /-!
diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean
index e52d4635d128a..3038a4f3dda83 100644
--- a/src/group_theory/sylow.lean
+++ b/src/group_theory/sylow.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
 
-import data.nat.factorization
+import data.nat.factorization.basic
 import data.set_like.fintype
 import group_theory.group_action.conj_act
 import group_theory.p_group
diff --git a/src/number_theory/arithmetic_function.lean b/src/number_theory/arithmetic_function.lean
index 1a2baae8badc2..f8e832f44c2d1 100644
--- a/src/number_theory/arithmetic_function.lean
+++ b/src/number_theory/arithmetic_function.lean
@@ -7,7 +7,7 @@ import algebra.big_operators.ring
 import number_theory.divisors
 import data.nat.squarefree
 import algebra.invertible
-import data.nat.factorization
+import data.nat.factorization.basic
 
 /-!
 # Arithmetic Functions and Dirichlet Convolution
diff --git a/src/number_theory/padics/padic_val.lean b/src/number_theory/padics/padic_val.lean
index 80fd6b1f19230..f6ec21be7c24d 100644
--- a/src/number_theory/padics/padic_val.lean
+++ b/src/number_theory/padics/padic_val.lean
@@ -9,7 +9,7 @@ import ring_theory.int.basic
 import tactic.basic
 import tactic.ring_exp
 import number_theory.divisors
-import data.nat.factorization
+import data.nat.factorization.basic
 
 /-!
 # p-adic Valuation
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 64b509ce77a60..6f617456d61a0 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis, Chris Hughes
 import algebra.associated
 import algebra.big_operators.basic
 import ring_theory.valuation.basic
-import data.nat.factorization
+import data.nat.factorization.basic
 
 /-!
 # Multiplicity of a divisor