generalise to unique factorization monoids

Mathlib.lean

@@ -477,8 +477,8 @@ import Mathlib.Algebra.Ring.ULift
 import Mathlib.Algebra.Ring.Units
 import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Algebra.SquareFree.Basic
-import Mathlib.Algebra.SquareFree.UniqueFactorizationDomain
+import Mathlib.Algebra.Squarefree.Basic
+import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
 import Mathlib.Algebra.Star.Basic
 import Mathlib.Algebra.Star.BigOperators
 import Mathlib.Algebra.Star.CHSH

Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2024 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import Mathlib.Algebra.Squarefree.Basic
+import Mathlib.RingTheory.UniqueFactorizationDomain
+
+/-!
+# Square-free elements of unique factorization monoids
+
+## Main results:
+ * `squarefree_mul_iff`: `x * y` is square-free iff `x` and `y` have no common factors and are
+   themselves square-free.
+
+-/
+
+variable {R : Type*} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x y p d : R}
+
+open UniqueFactorizationMonoid
+
+theorem squarefree_iff (hx₀ : x ≠ 0) (hxu : ¬ IsUnit x) :
+    Squarefree x ↔ ∀ p, Prime p → ¬ (p * p ∣ x) := by
+  refine ⟨fun h p hp hp' ↦ hp.not_unit (h p hp'), fun h d hd ↦ ?_⟩
+  induction' d using induction_on_prime with u hu z p _ hp _
+  · obtain ⟨p, hp⟩ := exists_prime_iff.mpr ⟨x, ⟨hx₀, hxu⟩⟩
+    rw [mul_zero, zero_dvd_iff] at hd
+    simpa [hd] using h p hp
+  · assumption
+  · specialize h p hp
+    replace hd : p * p ∣ x := by rw [mul_mul_mul_comm] at hd; exact dvd_of_mul_right_dvd hd
+    contradiction
+
+namespace Squarefree
+
+theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ}
+    (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
+    p ^ k ∣ y := by
+  nontriviality R
+  rcases eq_or_ne x 0 with rfl | hx₀
+  · have := not_squarefree_zero hx; contradiction
+  wlog hxu : ¬ IsUnit x
+  · rw [not_not] at hxu; rw [hxu.dvd_mul_left] at h; rw [pow_succ] at h; exact dvd_of_mul_left_dvd h
+  rw [squarefree_iff hx₀ hxu] at hx
+  by_cases hxp : p ∣ x
+  · obtain ⟨x', rfl⟩ := hxp
+    have hx' : ¬ p ∣ x' := by
+      specialize hx p hp
+      contrapose! hx
+      exact mul_dvd_mul_left p hx
+    replace h : p ^ k ∣ x' * y := by
+      rw [pow_succ, mul_assoc] at h
+      exact (mul_dvd_mul_iff_left hp.ne_zero).mp h
+    exact hp.pow_dvd_of_dvd_mul_left _ hx' h
+  · exact dvd_trans (pow_dvd_pow _ (k.le_add_right 1)) (hp.pow_dvd_of_dvd_mul_left _ hxp h)
+
+theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {k : ℕ}
+    (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
+    p ^ k ∣ x := by
+  rw [mul_comm] at h
+  exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h
+
+theorem dvd_of_squarefree_of_mul_dvd_mul_right
+    (hx : Squarefree x) (h : d * d ∣ x * y) :
+    d ∣ y := by
+  nontriviality R
+  rcases eq_or_ne x 0 with rfl | hx₀
+  · have := not_squarefree_zero hx; contradiction
+  induction' d using UniqueFactorizationMonoid.induction_on_coprime with u hu p k hp a b hab' ha hb
+  · simpa [hx₀] using h
+  · exact hu.dvd
+  · cases' k with k; · simp
+    apply pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hx hp
+    rw [← pow_add] at h
+    suffices p ^ ((k + 1) + 1) ∣ p ^ ((k + 1) + (k + 1)) by exact dvd_trans this h
+    apply pow_dvd_pow
+    omega
+  · rw [mul_mul_mul_comm] at h
+    exact mul_dvd_of_coprime hab' (ha <| dvd_of_mul_right_dvd h) (hb <| dvd_of_mul_left_dvd h)
+
+theorem dvd_of_squarefree_of_mul_dvd_mul_left
+    (hy : Squarefree y) (h : d * d ∣ x * y) :
+    d ∣ x := by
+  rw [mul_comm x y] at h
+  exact dvd_of_squarefree_of_mul_dvd_mul_right hy h
+
+end Squarefree
+
+theorem squarefree_mul_iff :
+    Squarefree (x * y) ↔ (∀ d, d ∣ x → d ∣ y → IsUnit d) ∧ Squarefree x ∧ Squarefree y := by
+  nontriviality R
+  refine ⟨fun h ↦ ⟨fun d hx hy ↦ h d (mul_dvd_mul hx hy),
+    h.of_mul_left, h.of_mul_right⟩, fun ⟨hxy, hx, hy⟩ ↦ ?_⟩
+  intro d
+  induction' d using UniqueFactorizationMonoid.induction_on_prime with _ hu _ p _ hp _
+  · simp [hx.ne_zero, hy.ne_zero]
+  · exact fun _ ↦ hu
+  · intro contra
+    exfalso
+    apply hp.not_unit
+    suffices p ∣ x ∧ p ∣ y by exact hxy p this.1 this.2
+    replace contra : p * p ∣ x * y := by
+      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⟩

Mathlib/Data/Nat/Squarefree.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.Algebra.SquareFree.Basic
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.Nat.Factorization.PrimePow
 import Mathlib.RingTheory.Int.Basic
 

Mathlib/FieldTheory/Perfect.lean

@@ -6,7 +6,7 @@ Authors: Oliver Nash
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.Algebra.CharP.Reduced
-import Mathlib.Algebra.SquareFree.UniqueFactorizationDomain
+import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
 
 /-!
 
@@ -233,10 +233,12 @@ theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g := by
     rcases hpn.eq_zero_or_one_of_pow_of_not_isUnit hp.not_unit with rfl | rfl; · simp
     exact (pow_one p).symm ▸ PerfectField.separable_of_irreducible hp.irreducible
   · intro hpq'
-    classical
-    have := EuclideanDomain.gcdMonoid K[X]
     obtain ⟨h, hp, hq⟩ := squarefree_mul_iff.mp hpq'
-    exact (ihp hp).mul (ihq hq) h
+    apply (ihp hp).mul (ihq hq)
+    classical
+    apply EuclideanDomain.isCoprime_of_dvd
+    · rintro ⟨rfl, rfl⟩; simp at hp
+    · exact fun d hd _ hdp hdq ↦ mem_nonunits_iff.mpr hd <| h d hdp hdq
 
 end PerfectField
 

Mathlib/FieldTheory/Separable.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.SquareFree.Basic
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.Polynomial.Expand
 import Mathlib.Data.Polynomial.Splits
 import Mathlib.FieldTheory.Minpoly.Field

Mathlib/RingTheory/ChainOfDivisors.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Paul Lezeau
 -/
 import Mathlib.Algebra.IsPrimePow
-import Mathlib.Algebra.SquareFree.Basic
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Order.Hom.Bounded
 import Mathlib.Algebra.GCDMonoid.Basic
 

Mathlib/RingTheory/Coprime/Basic.lean

@@ -98,12 +98,14 @@ theorem isCoprime_one_right : IsCoprime x 1 :=
   ⟨0, 1, by rw [one_mul, zero_mul, zero_add]⟩
 #align is_coprime_one_right isCoprime_one_right
 
+/-- See also `UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_right`. -/
 theorem IsCoprime.dvd_of_dvd_mul_right (H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y := by
   let ⟨a, b, H⟩ := H1
   rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
   exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
 #align is_coprime.dvd_of_dvd_mul_right IsCoprime.dvd_of_dvd_mul_right
 
+/-- See also `UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_left`. -/
 theorem IsCoprime.dvd_of_dvd_mul_left (H1 : IsCoprime x y) (H2 : x ∣ y * z) : x ∣ z := by
   let ⟨a, b, H⟩ := H1
   rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
@@ -127,6 +129,7 @@ theorem IsCoprime.mul_right (H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprim
   exact H1.mul_left H2
 #align is_coprime.mul_right IsCoprime.mul_right
 
+/-- See also `UniqueFactorizationMonoid.mul_dvd`. -/
 theorem IsCoprime.mul_dvd (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z := by
   obtain ⟨a, b, h⟩ := H
   rw [← mul_one z, ← h, mul_add]

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -197,6 +197,15 @@ theorem exists_prime_factors (a : α) :
   apply WfDvdMonoid.exists_factors a
 #align unique_factorization_monoid.exists_prime_factors UniqueFactorizationMonoid.exists_prime_factors
 
+lemma exists_prime_iff :
+    (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬ IsUnit x := by
+  refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
+  obtain ⟨f, hf, hf'⟩ := exists_prime_factors x hx₀
+  rcases f.empty_or_exists_mem with rfl | h
+  · have := associated_one_iff_isUnit.mp hf'.symm; contradiction
+  · obtain ⟨p, hp⟩ := h
+    exact ⟨p, hf _ hp⟩
+
 @[elab_as_elim]
 theorem induction_on_prime {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ x : α, IsUnit x → P x)
     (h₃ : ∀ a p : α, a ≠ 0 → Prime p → P a → P (p * a)) : P a := by
@@ -1212,6 +1221,45 @@ theorem multiplicative_of_coprime (f : α → β) (a b : α) (h0 : f 0 = 0)
 
 end Multiplicative
 
+section Coprime
+
+variable {x y d : R}
+
+/-- See also `IsCoprime.dvd_of_dvd_mul_left`. -/
+theorem dvd_of_coprime_of_dvd_mul_left
+    (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ x * d) : y ∣ d := by
+  rcases eq_or_ne x 0 with rfl | hx
+  · replace h : IsUnit y := h y (dvd_zero y) (refl _); exact h.dvd
+  rcases eq_or_ne y 0 with rfl | hy
+  · simp only [zero_dvd_iff, mul_eq_zero, hx, false_or] at h'; simp [h']
+  induction' y using UniqueFactorizationMonoid.induction_on_coprime
+    with u hu p k hp a b _ ha hb generalizing x d
+  · simpa [hx] using h'
+  · exact hu.dvd
+  · rcases eq_or_ne k 0 with rfl | hk; · simp
+    replace h : ¬ p ∣ x := fun contra ↦ hp.not_unit <| h p contra (dvd_pow_self p hk)
+    exact Prime.pow_dvd_of_dvd_mul_left hp k h h'
+  · rw [ne_eq, mul_eq_zero, not_or] at hy
+    have hxa : ∀ p, p ∣ x → p ∣ a → IsUnit p := fun p h₁ h₂ ↦ h p h₁ (h₂.mul_right b)
+    have hxb : ∀ p, p ∣ x → p ∣ b → IsUnit p := fun p h₁ h₂ ↦ h p h₁ (h₂.mul_left a)
+    obtain ⟨a', rfl⟩ := @ha x d hxa (dvd_of_mul_right_dvd h') hx hy.1
+    rw [mul_left_comm, mul_dvd_mul_iff_left hy.1] at h'
+    exact mul_dvd_mul_left a (@hb x a' hxb h' hx hy.2)
+
+/-- See also `IsCoprime.dvd_of_dvd_mul_right`. -/
+theorem dvd_of_coprime_of_dvd_mul_right
+    (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ d * x) : y ∣ d := by
+  rw [mul_comm] at h'; exact dvd_of_coprime_of_dvd_mul_left h h'
+
+/-- See also `IsCoprime.mul_dvd`. -/
+theorem mul_dvd_of_coprime (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (hx : x ∣ d) (hy : y ∣ d) :
+    x * y ∣ d := by
+  obtain ⟨x', rfl⟩ := hx
+  suffices y ∣ x' by exact mul_dvd_mul_left x this
+  exact dvd_of_coprime_of_dvd_mul_left h hy
+
+end Coprime
+
 end UniqueFactorizationMonoid
 
 namespace Associates

Mathlib/RingTheory/ZMod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
-import Mathlib.Algebra.SquareFree.Basic
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.ZMod.Basic
 import Mathlib.RingTheory.Int.Basic