From b622d4dfd1285f937c39d131399f8cd84b38ba8b Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 15 Mar 2022 18:38:06 +0000
Subject: [PATCH] chore(algebra/associated): move prime_dvd_prime_iff_eq
 (#12706)

---
 src/algebra/associated.lean | 5 +++++
 src/data/list/prime.lean    | 3 ---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
index 7e9b81e3742be..89bbca4533a9e 100644
--- a/src/algebra/associated.lean
+++ b/src/algebra/associated.lean
@@ -432,6 +432,11 @@ end
 theorem associated_eq_eq : (associated : α → α → Prop) = eq :=
 by { ext, rw associated_iff_eq }
 
+lemma prime_dvd_prime_iff_eq
+  {M : Type*} [cancel_comm_monoid_with_zero M] [unique Mˣ] {p q : M} (pp : prime p) (qp : prime q) :
+  p ∣ q ↔ p = q :=
+by rw [pp.dvd_prime_iff_associated qp, ←associated_eq_eq]
+
 end unique_units
 
 /-- The quotient of a monoid by the `associated` relation. Two elements `x` and `y`
diff --git a/src/data/list/prime.lean b/src/data/list/prime.lean
index bf6c5986e54c9..9fa1305b4c410 100644
--- a/src/data/list/prime.lean
+++ b/src/data/list/prime.lean
@@ -46,9 +46,6 @@ section cancel_comm_monoid_with_zero
 
 variables {M : Type*} [cancel_comm_monoid_with_zero M] [unique (units M)]
 
-lemma prime_dvd_prime_iff_eq {p q : M} (pp : prime p) (qp : prime q) : p ∣ q ↔ p = q :=
-by rw [pp.dvd_prime_iff_associated qp, ←associated_eq_eq]
-
 lemma mem_list_primes_of_dvd_prod {p : M} (hp : prime p) {L : list M} (hL : ∀ q ∈ L, prime q)
   (hpL : p ∣ L.prod) : p ∈ L :=
 begin