feat: add lemma exists_squarefree_dvd_pow_of_ne_zero (#10241)

leanprover-community · Feb 5, 2024 · ad95668 · ad95668
1 parent 65a5ead
commit ad95668
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean
@@ -728,6 +728,14 @@ theorem Associated.of_pow_associated_of_prime' [CancelCommMonoidWithZero α] {p
   (h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm
 #align associated.of_pow_associated_of_prime' Associated.of_pow_associated_of_prime'
 
+/-- See also `Irreducible.coprime_iff_not_dvd`. -/
+lemma Irreducible.coprime_iff_not_dvd' [Monoid α] {p n : α} (hp : Irreducible p) :
+    (∀ d, d ∣ p → d ∣ n → IsUnit d) ↔ ¬ p ∣ n := by
+  refine ⟨fun h contra ↦ hp.not_unit (h p (refl _) contra), fun hpn d hdp hdn ↦ ?_⟩
+  contrapose! hpn
+  suffices Associated p d from this.dvd.trans hdn
+  exact (hp.dvd_iff.mp hdp).resolve_left hpn
+
 section UniqueUnits
 
 variable [Monoid α] [Unique αˣ]

diff --git a/Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean b/Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean
@@ -94,3 +94,18 @@ theorem squarefree_mul_iff :
       rw [mul_mul_mul_comm] at contra; exact dvd_of_mul_right_dvd contra
     exact ⟨hy.dvd_of_squarefree_of_mul_dvd_mul_left contra,
       hx.dvd_of_squarefree_of_mul_dvd_mul_right contra⟩
+
+lemma exists_squarefree_dvd_pow_of_ne_zero (hx : x ≠ 0) :
+    ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n := by
+  induction' x using WfDvdMonoid.induction_on_irreducible with u hu z p hz hp ih
+  · contradiction
+  · exact ⟨1, 0, squarefree_one, one_dvd u, hu.dvd⟩
+  · obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
+    rcases n.eq_zero_or_pos with rfl | hn
+    · exact ⟨p, 1, hp.squarefree, dvd_mul_right p z, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
+    by_cases hp' : p ∣ y
+    · exact ⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
+        mul_comm p z ▸ pow_succ' y n ▸ mul_dvd_mul hy' hp'⟩
+    · suffices Squarefree (p * y) from ⟨p * y, n, this,
+        mul_dvd_mul_left p hyx, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
+      exact squarefree_mul_iff.mpr ⟨hp.coprime_iff_not_dvd'.mpr hp', hp.squarefree, hy⟩
diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean
@@ -454,6 +454,7 @@ theorem Prime.coprime_iff_not_dvd {p n : R} (pp : Prime p) : IsCoprime p n ↔
   pp.irreducible.coprime_iff_not_dvd
 #align prime.coprime_iff_not_dvd Prime.coprime_iff_not_dvd
 
+/-- See also `Irreducible.coprime_iff_not_dvd'`. -/
 theorem Irreducible.dvd_iff_not_coprime {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n :=
   iff_not_comm.2 hp.coprime_iff_not_dvd
 #align irreducible.dvd_iff_not_coprime Irreducible.dvd_iff_not_coprime