refactor(data/nat/prime): mem_factors_iff_dvd (#272)

Author: ChrisHughes24

data/list/basic.lean

@@ -1173,6 +1173,10 @@ theorem prod_erase [decidable_eq α] [comm_monoid α] {a} :
     { simp [ne.symm, list.erase, prod_erase h, mul_left_comm a b] }
   end
 
+lemma dvd_prod [comm_semiring α] {a} {l : list α} (ha : a ∈ l) : a ∣ l.prod :=
+let ⟨s, t, h⟩ := mem_split ha in
+by rw [h, prod_append, prod_cons, mul_left_comm]; exact dvd_mul_right _ _
+
 @[simp] theorem sum_const_nat (m n : ℕ) : sum (list.repeat m n) = m * n :=
 by induction n; simp [*, nat.mul_succ]
 

data/nat/prime.lean

@@ -321,8 +321,9 @@ lemma mem_list_primes_of_dvd_prod {p : ℕ} (hp : prime p) :
     (λ h, have hl : ∀ p ∈ l, prime p := λ p hlp, h₁ p ((mem_cons_iff _ _ _).2 (or.inr hlp)),
     (mem_cons_iff _ _ _).2 (or.inr (mem_list_primes_of_dvd_prod hl h)))
 
-lemma mem_factors_of_dvd {n p : ℕ} (hn : 0 < n) (hp : prime p) (h : p ∣ n) : p ∈ factors n :=
-mem_list_primes_of_dvd_prod hp (@mem_factors n) ((prod_factors hn).symm ▸ h)
+lemma mem_factors_iff_dvd {n p : ℕ} (hn : 0 < n) (hp : prime p) : p ∈ factors n ↔ p ∣ n :=
+⟨λ h, prod_factors hn ▸ list.dvd_prod h,
+ λ h, mem_list_primes_of_dvd_prod hp (@mem_factors n) ((prod_factors hn).symm ▸ h)⟩
 
 lemma perm_of_prod_eq_prod : ∀ {l₁ l₂ : list ℕ}, prod l₁ = prod l₂ →
   (∀ p ∈ l₁, prime p) → (∀ p ∈ l₂, prime p) → l₁ ~ l₂