chore(algebra/associated): move prime_dvd_prime_iff_eq (#12706)

leanprover-community · Mar 15, 2022 · b622d4d · b622d4d
1 parent 7ed4f2c
commit b622d4d
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git 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
@@ -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