refactor(data/nat/factorization): Change definition of `factorization…

…` to be computable (#12301)

This PR changes the definition of `data.nat.factorization` to not depend on `multiset.to_finsupp` and instead to depend on `padic_val_nat`. This sidesteps the computability issues with finsupp discussed in [this thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.60ite.60.20with.20multiple.20decidable.20instances/near/272409877).

To deal with the changed imports this PR also moves some material from `number_theory/padics/padic_val` and `ring_theory/multiplicity` into `data/nat/factorization/basic`. 

Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>



Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>

src/analysis/special_functions/log/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
 import analysis.special_functions.exp
+import data.nat.factorization.basic
 
 /-!
 # Real logarithm

src/data/nat/choose/factorization.lean

@@ -5,7 +5,7 @@ Authors: Bolton Bailey, Patrick Stevens, Thomas Browning
 -/
 
 import data.nat.choose.central
-import number_theory.padics.padic_norm
+import data.nat.factorization.basic
 import data.nat.multiplicity
 
 /-!
@@ -38,7 +38,7 @@ begin
   by_cases h : (choose n k).factorization p = 0, { simp [h] },
   have hp : p.prime := not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h,
   have hkn : k ≤ n, { refine le_of_not_lt (λ hnk, h _), simp [choose_eq_zero_of_lt hnk] },
-  rw [←@padic_val_nat_eq_factorization p _ ⟨hp⟩, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
+  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
   simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe],
   refine (finset.card_filter_le _ _).trans (le_of_eq (nat.card_Ico _ _)),
 end
@@ -73,7 +73,7 @@ begin
   { exact factorization_eq_zero_of_non_prime (choose n k) hp },
   cases lt_or_le n k with hnk hkn,
   { simp [choose_eq_zero_of_lt hnk] },
-  rw [←@padic_val_nat_eq_factorization p _ ⟨hp⟩, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
+  rw [factorization_def _ hp, @padic_val_nat_def _ ⟨hp⟩ _ (choose_pos hkn)],
   simp only [hp.multiplicity_choose hkn (lt_add_one _), part_enat.get_coe,
     finset.card_eq_zero, finset.filter_eq_empty_iff, not_le],
   intros i hi,

src/data/nat/factorization/basic.lean

@@ -3,9 +3,10 @@ Copyright (c) 2021 Stuart Presnell. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stuart Presnell
 -/
-import data.nat.prime
-import data.finsupp.multiset
 import algebra.big_operators.finsupp
+import data.finsupp.multiset
+import data.nat.prime
+import number_theory.padics.padic_val
 import data.nat.interval
 
 /-!
@@ -42,23 +43,52 @@ namespace nat
 
 /-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
  mapping each prime factor of `n` to its multiplicity in `n`. -/
-noncomputable def factorization (n : ℕ) : ℕ →₀ ℕ := (n.factors : multiset ℕ).to_finsupp
+def factorization (n : ℕ) : ℕ →₀ ℕ :=
+{ support := n.factors.to_finset,
+  to_fun := λ p, if p.prime then padic_val_nat p n else 0,
+  mem_support_to_fun :=
+      begin
+        rcases eq_or_ne n 0 with rfl | hn0, { simp },
+        simp only [mem_factors hn0, mem_to_finset, ne.def, ite_eq_right_iff, not_forall,
+          exists_prop, and.congr_right_iff],
+        rintro p hp,
+        haveI := fact_iff.mpr hp,
+        exact dvd_iff_padic_val_nat_ne_zero hn0,
+      end }
+
+lemma factorization_def (n : ℕ) {p : ℕ} (pp : p.prime) : n.factorization p = padic_val_nat p n :=
+by simpa [factorization] using absurd pp
+
+/-- We can write both `n.factorization p` and `n.factors.count p` to represent the power
+of `p` in the factorization of `n`: we declare the former to be the simp-normal form. -/
+@[simp] lemma factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p :=
+begin
+  rcases n.eq_zero_or_pos with rfl | hn0, { simp [factorization] },
+  by_cases pp : p.prime, swap,
+  { rw count_eq_zero_of_not_mem (mt prime_of_mem_factors pp), simp [factorization, pp] },
+  simp only [factorization, coe_mk, pp, if_true],
+  rw [←part_enat.coe_inj, padic_val_nat_def' pp.ne_one hn0,
+    unique_factorization_monoid.multiplicity_eq_count_normalized_factors pp hn0.ne'],
+  simp [factors_eq],
+end
+
+lemma factorization_eq_factors_multiset (n : ℕ) :
+  n.factorization = (n.factors : multiset ℕ).to_finsupp :=
+by { ext p, simp }
+
+lemma multiplicity_eq_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
+  multiplicity p n = n.factorization p :=
+by simp [factorization, pp, (padic_val_nat_def' pp.ne_one hn.bot_lt)]
 
 /-! ### Basic facts about factorization -/
 
 @[simp] lemma factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : n.factorization.prod pow = n :=
 begin
+  rw factorization_eq_factors_multiset n,
   simp only [←prod_to_multiset, factorization, multiset.coe_prod, multiset.to_finsupp_to_multiset],
   exact prod_factors hn,
 end
 
-/-- We can write both `n.factorization p` and `n.factors.count p` to represent the power
-of `p` in the factorization of `n`: we declare the former to be the simp-normal form.
-However, since `factorization` is a finsupp it's noncomputable.  This theorem can also
-be used in reverse to compute values of `factorization n p` when required. -/
-@[simp] lemma factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p :=
-by simp [factorization]
-
 lemma eq_of_factorization_eq {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
   (h : ∀ p : ℕ, a.factorization p = b.factorization p) : a = b :=
 eq_of_perm_factors ha hb (by simpa only [list.perm_iff_count, factors_count_eq] using h)
@@ -68,14 +98,14 @@ lemma factorization_inj : set.inj_on factorization { x : ℕ | x ≠ 0 } :=
 λ a ha b hb h, eq_of_factorization_eq ha hb (λ p, by simp [h])
 
 @[simp] lemma factorization_zero : factorization 0 = 0 :=
-by simp [factorization]
+by simpa [factorization]
 
 @[simp] lemma factorization_one : factorization 1 = 0 :=
-by simp [factorization]
+by simpa [factorization]
 
 /-- The support of `n.factorization` is exactly `n.factors.to_finset` -/
 @[simp] lemma support_factorization {n : ℕ} : n.factorization.support = n.factors.to_finset :=
-by simp [factorization, multiset.to_finsupp_support]
+by simp [factorization]
 
 lemma factor_iff_mem_factorization {n p : ℕ} : p ∈ n.factorization.support ↔ p ∈ n.factors :=
 by simp only [support_factorization, list.mem_to_finset]
@@ -111,7 +141,10 @@ by rwa [←factors_count_eq, count_pos, mem_factors_iff_dvd hn hp]
 
 /-- The only numbers with empty prime factorization are `0` and `1` -/
 lemma factorization_eq_zero_iff (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1 :=
-by simp [factorization, add_equiv.map_eq_zero_iff, multiset.coe_eq_zero]
+begin
+  rw factorization_eq_factors_multiset n,
+  simp [factorization, add_equiv.map_eq_zero_iff, multiset.coe_eq_zero],
+end
 
 lemma factorization_eq_zero_iff' (n p : ℕ) :
   n.factorization p = 0 ↔ ¬p.prime ∨ ¬p ∣ n ∨ n = 0 :=
@@ -203,7 +236,6 @@ lemma eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : 
  λ h, by rw [←h, prod_pow_factorization_eq_self hf]⟩
 
 /-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes. -/
-noncomputable
 def factorization_equiv : ℕ+ ≃ {f : ℕ →₀ ℕ | ∀ p ∈ f.support, prime p} :=
 { to_fun    := λ ⟨n, hn⟩, ⟨n.factorization, λ _, prime_of_mem_factorization⟩,
   inv_fun   := λ ⟨f, hf⟩, ⟨f.prod pow,
@@ -251,7 +283,7 @@ end
 lemma factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b :=
 begin
   rcases eq_or_ne n 0 with rfl | hn, { simp },
-  by_cases pp : p.prime, 
+  by_cases pp : p.prime,
   { exact (pow_le_iff_le_right pp.two_le).1 (le_trans (pow_factorization_le p hn) hb) },
   { simp [factorization_eq_zero_of_non_prime n pp] }
 end
@@ -401,6 +433,19 @@ begin
     simp [←factorization_le_iff_dvd he_pos hd_pos, h1, hea', heb'] },
 end
 
+@[to_additive sum_factors_gcd_add_sum_factors_mul]
+lemma prod_factors_gcd_mul_prod_factors_mul {β : Type*} [comm_monoid β] (m n : ℕ) (f : ℕ → β) :
+  (m.gcd n).factors.to_finset.prod f * (m * n).factors.to_finset.prod f
+    = m.factors.to_finset.prod f * n.factors.to_finset.prod f :=
+begin
+  rcases eq_or_ne n 0 with rfl | hm0, { simp },
+  rcases eq_or_ne m 0 with rfl | hn0, { simp },
+  rw [←@finset.prod_union_inter _ _ m.factors.to_finset n.factors.to_finset, mul_comm],
+  congr,
+  { apply factors_mul_to_finset; assumption },
+  { simp only [←support_factorization, factorization_gcd hn0 hm0, finsupp.support_inf] },
+end
+
 lemma set_of_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
   {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} = set.Icc 1 (n.factorization p) :=
 by { ext, simp [lt_succ_iff, one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn] }
@@ -576,4 +621,34 @@ begin
     convert (factorization_disjoint_of_coprime hab) },
 end
 
+/-- Two positive naturals are equal if their prime padic valuations are equal -/
+lemma eq_iff_prime_padic_val_nat_eq (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
+  a = b ↔ (∀ p : ℕ, p.prime → padic_val_nat p a = padic_val_nat p b) :=
+begin
+  split,
+  { rintros rfl, simp },
+  { intro h,
+    refine eq_of_factorization_eq ha hb (λ p, _),
+    by_cases pp : p.prime,
+    { simp [factorization_def, pp, h p pp] },
+    { simp [factorization_eq_zero_of_non_prime, pp] } },
+end
+
+lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
+  ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
+begin
+  nth_rewrite_rhs 0 ←factorization_prod_pow_eq_self hn,
+  rw eq_comm,
+  apply finset.prod_subset_one_on_sdiff,
+  { exact λ p hp, finset.mem_filter.mpr
+      ⟨finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
+       prime_of_mem_factorization hp⟩ },
+  { intros p hp,
+    cases finset.mem_sdiff.mp hp with hp1 hp2,
+    rw ←factorization_def n (finset.mem_filter.mp hp1).2,
+    simp [finsupp.not_mem_support_iff.mp hp2] },
+  { intros p hp,
+    simp [factorization_def n (prime_of_mem_factorization hp)] }
+end
+
 end nat

src/data/nat/totient.lean

@@ -3,13 +3,10 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import algebra.big_operators.basic
-import data.nat.prime
-import data.zmod.basic
-import ring_theory.multiplicity
-import data.nat.periodic
 import algebra.char_p.two
-import number_theory.divisors
+import data.nat.factorization.basic
+import data.nat.periodic
+import data.zmod.basic
 
 /-!
 # Euler's totient function

src/group_theory/exponent.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
 import group_theory.order_of_element
-import algebra.punit_instances
 import algebra.gcd_monoid.finset
+import algebra.punit_instances
+import data.nat.factorization.basic
 import tactic.by_contra
-import number_theory.padics.padic_val
 
 /-!
 # Exponent of a group

src/number_theory/padics/padic_val.lean

@@ -9,7 +9,6 @@ import ring_theory.int.basic
 import tactic.basic
 import tactic.ring_exp
 import number_theory.divisors
-import data.nat.factorization.basic
 
 /-!
 # p-adic Valuation
@@ -237,6 +236,11 @@ begin
   solve_by_elim,
 end
 
+lemma dvd_iff_padic_val_nat_ne_zero {p n : ℕ} [fact p.prime] (hn0 : n ≠ 0) :
+  (p ∣ n) ↔ padic_val_nat p n ≠ 0 :=
+⟨λ h, one_le_iff_ne_zero.mp (one_le_padic_val_nat_of_dvd hn0.bot_lt h),
+ λ h, not_not.1 (mt padic_val_nat.eq_zero_of_not_dvd h)⟩
+
 end padic_val_nat
 
 namespace padic_val_rat
@@ -510,35 +514,8 @@ protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
       { exact hc } },
   end
 
-lemma padic_val_nat_eq_factorization (p n : ℕ) [hp : fact p.prime] :
-  padic_val_nat p n = n.factorization p :=
-begin
-  by_cases hn : n = 0, { subst hn, simp },
-  rw @padic_val_nat_def p _ n (nat.pos_of_ne_zero hn),
-  simp [@multiplicity_eq_factorization n p hp.elim hn],
-end
-
 open_locale big_operators
 
-lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
-  ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
-begin
-  nth_rewrite_rhs 0 ←factorization_prod_pow_eq_self hn,
-  rw eq_comm,
-  apply finset.prod_subset_one_on_sdiff,
-  { exact λ p hp, finset.mem_filter.mpr
-      ⟨finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
-       prime_of_mem_factorization hp⟩ },
-  { intros p hp,
-    cases finset.mem_sdiff.mp hp with hp1 hp2,
-    haveI := fact_iff.mpr (finset.mem_filter.mp hp1).2,
-    rw padic_val_nat_eq_factorization p n,
-    simp [finsupp.not_mem_support_iff.mp hp2] },
-  { intros p hp,
-    haveI := fact_iff.mpr (prime_of_mem_factorization hp),
-    simp [padic_val_nat_eq_factorization] }
-end
-
 lemma range_pow_padic_val_nat_subset_divisors {n : ℕ} (p : ℕ) (hn : n ≠ 0) :
   (finset.range (padic_val_nat p n + 1)).image (pow p) ⊆ n.divisors :=
 begin

src/ring_theory/multiplicity.lean

@@ -6,7 +6,6 @@ Authors: Robert Y. Lewis, Chris Hughes
 import algebra.associated
 import algebra.big_operators.basic
 import ring_theory.valuation.basic
-import data.nat.factorization.basic
 
 /-!
 # Multiplicity of a divisor
@@ -513,21 +512,4 @@ begin
   exact hp this
 end
 
-lemma multiplicity_eq_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
-  multiplicity p n = n.factorization p :=
-multiplicity.eq_coe_iff.mpr ⟨pow_factorization_dvd n p, pow_succ_factorization_not_dvd hn pp⟩
-
-@[to_additive sum_factors_gcd_add_sum_factors_mul]
-lemma prod_factors_gcd_mul_prod_factors_mul {β : Type*} [comm_monoid β] (m n : ℕ) (f : ℕ → β) :
-  (m.gcd n).factors.to_finset.prod f * (m * n).factors.to_finset.prod f
-    = m.factors.to_finset.prod f * n.factors.to_finset.prod f :=
-begin
-  rcases eq_or_ne n 0 with rfl | hm0, { simp },
-  rcases eq_or_ne m 0 with rfl | hn0, { simp },
-  rw [←@finset.prod_union_inter _ _ m.factors.to_finset n.factors.to_finset, mul_comm],
-  congr,
-  { apply factors_mul_to_finset; assumption },
-  { simp only [←support_factorization, factorization_gcd hn0 hm0, finsupp.support_inf] },
-end
-
 end nat