feat(Data/Nat): a number divides a power of its own radical (#40170)

A few factorization lemmas, including:
- `∀ n : ℕ`, `n ∣ radical n ^ n`
- `∀ n k : ℕ`, `n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors`
- `∀ n k : ℕ`, `radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors`
- In any `UniqueFactorizationMonoid M`, `∀ a : M`, `∃ n, a ∣ radical a ^ n`

[#Is there code for X? > A number divides a power of its square-free component](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/A.20number.20divides.20a.20power.20of.20its.20square-free.20component/with/599339469)

Author: SnirBroshi

Mathlib/Algebra/Order/Group/Multiset.lean

@@ -63,6 +63,12 @@ lemma mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0
 lemma mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s := by
   simp [*]
 
+theorem smul_subset_self (s : Multiset α) (n : ℕ) : n • s ⊆ s :=
+  subset_iff.mpr fun _ ↦ mem_of_mem_nsmul
+
+theorem subset_smul_self_of_ne_zero (s : Multiset α) {n : ℕ} (hn : n ≠ 0) : s ⊆ n • s :=
+  subset_iff.mpr fun _ ↦ mem_nsmul_of_ne_zero hn |>.mpr
+
 lemma nsmul_cons {s : Multiset α} (n : ℕ) (a : α) :
     n • (a ::ₘ s) = n • ({a} : Multiset α) + n • s := by
   rw [← singleton_add, nsmul_add]
@@ -180,6 +186,14 @@ lemma count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by
 
 end
 
+theorem le_card_smul_iff_subset {s t : Multiset α} : s ≤ s.card • t ↔ s ⊆ t := by
+  classical
+  refine ⟨fun hle ↦ Subset.trans (subset_of_le hle) (t.smul_subset_self s.card), ?_⟩
+  refine fun hsub ↦ le_iff_count.mpr fun a ↦ ?_
+  by_cases! has : a ∉ s
+  · simp [count_eq_zero_of_notMem has]
+  grw [count_le_card, count_nsmul, ← one_le_count_iff_mem.mpr <| mem_of_subset hsub has, mul_one]
+
 -- TODO: This should be `addMonoidHom_ext`
 @[ext]
 lemma addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g := by
@@ -189,14 +203,6 @@ lemma addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f
   | cons a s ih => simp only [← singleton_add, _root_.map_add, ih, h]
 
 theorem le_smul_dedup [DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n • dedup s :=
-  ⟨(s.map fun a => count a s).fold max 0,
-    le_iff_count.2 fun a => by
-      rw [count_nsmul]; by_cases h : a ∈ s
-      · grw [← one_le_count_iff_mem.2 <| mem_dedup.2 h]
-        have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
-          simp
-        rw [cons_erase h] at this
-        simpa [mul_succ] using this
-      · simp [count_eq_zero.2 h, Nat.zero_le]⟩
+  ⟨s.card, le_card_smul_iff_subset.mpr s.subset_dedup⟩
 
 end Multiset

Mathlib/Data/Nat/Choose/Lucas.lean

@@ -208,7 +208,7 @@ theorem gcd_choose_eq_minFac_of_isPrimePow (h : IsPrimePow n) :
   have : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1 := by
     refine multiplicity_eq_of_dvd_of_not_dvd ?_ (minFac_sq_ndvd_gcd_choose_of_isPrimePow h)
     simpa using minFac_dvd_gcd_choose_of_isPrimePow h
-  rw [Nat.prod_pow_primeFactors_factorization ne_zero, primeFactors_gcd_choose_of_isPrimePow h]
+  rw [Nat.prod_primeFactors_coe_pow_factorization ne_zero, primeFactors_gcd_choose_of_isPrimePow h]
   simp [← Nat.multiplicity_eq_factorization isPrime ne_zero, this]
 
 /-- For a natural number `n` greater than `1`, assume that `n` is not a prime power, then

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -477,11 +477,16 @@ theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n <
   · intro p hp
     simp [factorization_def n (prime_of_mem_primeFactors hp)]
 
-lemma prod_pow_primeFactors_factorization (hn : n ≠ 0) :
+theorem prod_primeFactors_pow_factorization (hn : n ≠ 0) :
+    n = ∏ p ∈ n.primeFactors, p ^ n.factorization p :=
+  prod_factorization_pow_eq_self hn |>.symm.trans <| prod_factorization_eq_prod_primeFactors _
+
+lemma prod_primeFactors_coe_pow_factorization (hn : n ≠ 0) :
     n = ∏ (p : n.primeFactors), (p : ℕ) ^ (n.factorization p) := by
-  nth_rw 1 [← prod_factorization_pow_eq_self hn]
-  rw [prod_factorization_eq_prod_primeFactors _]
-  exact prod_subtype n.primeFactors (fun _ ↦ Iff.rfl) fun a ↦ a ^ n.factorization a
+  simpa using prod_primeFactors_pow_factorization hn
+
+@[deprecated (since := "2026-06-24")]
+alias prod_pow_primeFactors_factorization := prod_primeFactors_coe_pow_factorization
 
 lemma pairwise_coprime_pow_primeFactors_factorization :
     Pairwise (Function.onFun Nat.Coprime fun (p : n.primeFactors) ↦ p ^ n.factorization p) := by
@@ -491,6 +496,26 @@ lemma pairwise_coprime_pow_primeFactors_factorization :
   · exact Nat.prime_of_mem_primeFactors p1.2
   · exact Nat.prime_of_mem_primeFactors p2.2
 
+theorem dvd_prod_primeFactors_pow_self {n : ℕ} (hn : n ≠ 0) :
+    n ∣ (∏ p ∈ n.primeFactors, p) ^ n := by
+  nth_rw 1 [← Finset.prod_pow, prod_primeFactors_pow_factorization hn]
+  refine prod_dvd_prod_of_dvd _ _ fun i hi ↦ pow_dvd_pow i ?_
+  grw [n.factorization_def <| prime_of_mem_primeFactors hi, padicValNat_le_self]
+
+theorem dvd_pow_self_iff {n k : ℕ} (hn : n ≠ 0) (hk : k ≠ 0) :
+    n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · grw [← Nat.primeFactors_pow k hn, Nat.primeFactors_mono h <| pow_ne_zero n hk]
+  · grw [dvd_prod_primeFactors_pow_self hn, prod_dvd_prod_of_subset _ _ _ h, prod_primeFactors_dvd]
+
+theorem exists_dvd_pow_iff {n k : ℕ} (hn : n ≠ 0) (hk : k ≠ 0) :
+    (∃ m, n ∣ k ^ m) ↔ n.primeFactors ⊆ k.primeFactors := by
+  refine ⟨fun ⟨m, h⟩ ↦ ?_, fun h ↦ ⟨n, dvd_pow_self_iff hn hk |>.mpr h⟩⟩
+  rcases eq_or_ne m 0 with (rfl | hm)
+  · simp_all
+  rw [← Nat.primeFactors_pow k hm]
+  exact Nat.primeFactors_mono h <| pow_ne_zero m hk
+
 /-! ### Lemmas about factorizations of particular functions -/
 
 /-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.

Mathlib/Data/Nat/MaxPowDiv.lean

@@ -136,6 +136,19 @@ theorem pow_padicValNat_mul_divMaxPow (p n : ℕ) : p ^ padicValNat p n * divMax
 theorem _root_.pow_padicValNat_dvd {p n : ℕ} : p ^ padicValNat p n ∣ n :=
   ⟨divMaxPow n p, by simp⟩
 
+theorem padicValNat_lt_self {p n : ℕ} (hn : n ≠ 0) : padicValNat p n < n := by
+  match p with
+  | 0 | 1 => simp [Nat.pos_of_ne_zero hn]
+  | p + 2 =>
+    apply (p + 2 |>.pow_lt_pow_iff_right <| by lia).mp
+    apply Nat.lt_of_le_of_lt ?_ <| Nat.lt_pow_self <| by lia
+    exact le_of_dvd (Nat.pos_of_ne_zero hn) pow_padicValNat_dvd
+
+theorem padicValNat_le_self {p : ℕ} (n : ℕ) : padicValNat p n ≤ n := by
+  rcases eq_or_ne n 0 with rfl | hn
+  · simp
+  · exact Nat.le_of_lt <| padicValNat_lt_self hn
+
 theorem not_dvd_divMaxPow {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) : ¬p ∣ divMaxPow n p := by
   simp [divMaxPow, maxPowDvdDiv, maxPowDvdDiv.go_spec, *]
 

Mathlib/Data/Nat/Squarefree.lean

@@ -373,6 +373,16 @@ lemma primeFactors_prod (hs : ∀ p ∈ s, p.Prime) : primeFactors (∏ p ∈ s,
   rintro ⟨hp, q, hq, hpq⟩
   rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]
 
+theorem primeFactors_prod_primeFactors (n : ℕ) :
+    (∏ p ∈ n.primeFactors, p).primeFactors = n.primeFactors :=
+  primeFactors_prod fun _ hp ↦ n.mem_primeFactors.mp hp |>.left
+
+theorem prod_primeFactors_dvd_iff {n k : ℕ} (hk : k ≠ 0) :
+    (∏ p ∈ n.primeFactors, p) ∣ k ↔ n.primeFactors ⊆ k.primeFactors := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · grw [← Nat.primeFactors_mono h hk, primeFactors_prod_primeFactors]
+  · grw [← k.prod_primeFactors_dvd, Finset.prod_dvd_prod_of_subset _ _ _ h]
+
 lemma primeFactors_div_gcd (hm : Squarefree m) (hn : n ≠ 0) :
     primeFactors (m / m.gcd n) = primeFactors m \ primeFactors n := by
   ext p

Mathlib/Data/ZMod/QuotientRing.lean

@@ -87,7 +87,7 @@ def ZMod.prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ)
 /-- The **Chinese remainder theorem**, version for `ZMod n`. -/
 def ZMod.equivPi (hn : n ≠ 0) :
     ZMod n ≃+* Π (p : n.primeFactors), ZMod (p ^ (n.factorization p)) :=
-  (ringEquivCongr <| Nat.prod_pow_primeFactors_factorization hn).trans
+  (ringEquivCongr <| Nat.prod_primeFactors_coe_pow_factorization hn).trans
     <| prodEquivPi (fun (p : n.primeFactors) ↦ (p : ℕ) ^ (n.factorization p))
       n.pairwise_coprime_pow_primeFactors_factorization
 

Mathlib/RingTheory/Radical/Basic.lean

@@ -56,6 +56,12 @@ open scoped Classical in
 def primeFactors (a : M) : Finset M :=
   (normalizedFactors a).toFinset
 
+@[simp]
+theorem toFinset_normalizedFactors [DecidableEq M] :
+    (normalizedFactors a).toFinset = primeFactors a := by
+  unfold primeFactors
+  convert rfl
+
 lemma mem_primeFactors : a ∈ primeFactors b ↔ a ∈ normalizedFactors b := by
   simp only [primeFactors, Multiset.mem_toFinset]
 
@@ -296,6 +302,22 @@ theorem radical_dvd_iff_primeFactors_subset (hb : b ≠ 0) :
   rw [← dvd_radical_iff isRadical_radical hb,
     radical_dvd_radical_iff_primeFactors_subset_primeFactors]
 
+theorem exists_dvd_pow_iff_radical_dvd (ha : a ≠ 0) : (∃ n, a ∣ b ^ n) ↔ radical a ∣ b := by
+  rcases eq_or_ne b 0 with (rfl | hb)
+  · exact ⟨by simp, fun _ ↦ ⟨1, by simp⟩⟩
+  refine ⟨fun ⟨n, hdvd⟩ ↦ ?_, fun h ↦ ⟨normalizedFactors a |>.card, ?_⟩⟩
+  · rcases eq_or_ne n 0 with (rfl | hn)
+    · simp [radical_of_isUnit <| isUnit_of_dvd_one <| pow_zero b ▸ hdvd]
+    grw [radical_dvd_radical hdvd <| pow_ne_zero _ hb, radical_pow b hn, radical_dvd_self]
+  · classical
+    rwa [dvd_iff_normalizedFactors_le_normalizedFactors ha <| pow_ne_zero _ hb,
+      normalizedFactors_pow, Multiset.le_card_smul_iff_subset, ← Multiset.toFinset_subset,
+      toFinset_normalizedFactors, toFinset_normalizedFactors,
+      ← radical_dvd_iff_primeFactors_subset hb]
+
+theorem exists_dvd_radical_self_pow (ha : a ≠ 0) : ∃ n, a ∣ radical a ^ n := by
+  rw [exists_dvd_pow_iff_radical_dvd ha]
+
 /-- Radical is multiplicative for relatively prime elements. -/
 theorem radical_mul (hc : IsRelPrime a b) :
     radical (a * b) = radical a * radical b := by

Mathlib/RingTheory/Radical/NatInt.lean

@@ -6,12 +6,10 @@ Authors: Bhavik Mehta, Arend Mellendijk, Jeremy Tan
 module
 
 public import Mathlib.Algebra.EuclideanDomain.Int
-public import Mathlib.Algebra.GCDMonoid.Nat
 public import Mathlib.Data.Nat.Prime.Int
-public import Mathlib.Data.Nat.PrimeFin
+public import Mathlib.Data.Nat.Squarefree
 public import Mathlib.RingTheory.PrincipalIdealDomain
 public import Mathlib.RingTheory.Radical.Basic
-public import Mathlib.RingTheory.UniqueFactorizationDomain.Nat
 
 /-!
 # The radical in `ℕ` and `ℤ`
@@ -73,6 +71,16 @@ lemma radical_pos (n) : 0 < radical n := pos_of_ne_zero radical_ne_zero
 @[simp] lemma self_lt_radical_iff : n < radical n ↔ n = 0 := by
   simpa only [not_le, not_not] using radical_le_self_iff.not
 
+theorem primeFactors_radical (n : ℕ) : (radical n).primeFactors = n.primeFactors := by
+  rw [radical_eq_prod_primeFactors, primeFactors_prod_primeFactors]
+
+theorem radical_dvd_iff {n k : ℕ} (hk : k ≠ 0) :
+    radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors := by
+  rw [radical_eq_prod_primeFactors, prod_primeFactors_dvd_iff hk]
+
+theorem dvd_radical_pow_self {n : ℕ} (hn : n ≠ 0) : n ∣ radical n ^ n := by
+  grw [radical_eq_prod_primeFactors, ← dvd_prod_primeFactors_pow_self hn]
+
 open Qq Lean Mathlib.Meta Finset
 
 namespace Mathlib.Meta.Positivity