[Merged by Bors] - feat(data/nat/prime): prime.dvd_prod_iff; golf mem_list_primes_of_dvd_prod

src/algebra/associated.lean

@@ -719,3 +719,25 @@ dvd_and_not_dvd_iff.symm
 end cancel_comm_monoid_with_zero
 
 end associates
+
+namespace multiset
+
+lemma prod_ne_zero_of_prime [comm_cancel_monoid_with_zero α] [nontrivial α]
+ (s : multiset α) (h : ∀ x ∈ s, prime x) : s.prod ≠ 0 :=
+multiset.prod_ne_zero (λ h0, prime.ne_zero (h 0 h0) rfl)
+
+end multiset
+
+/-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L` -/
+lemma prime.dvd_prod_iff {M : Type*} [comm_monoid_with_zero M] {p : M} {L : list M} (pp : prime p) :
+p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a :=
+begin
+  split,
+  { intros h,
+    induction L,
+    { simp only [list.prod_nil] at h, exact absurd h (prime.not_dvd_one pp) },
+    { rw list.prod_cons at h,
+      cases (prime.dvd_or_dvd pp) h, { use L_hd, simp [h_1] },
+      { rcases L_ih h_1 with ⟨x, hx1, hx2⟩, use x, simp [list.mem_cons_iff, hx1, hx2] } } },
+  { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (list.dvd_prod ha1) },
+end

src/data/nat/prime.lean

@@ -490,6 +490,25 @@ theorem prime.not_dvd_mul {p m n : ℕ} (pp : prime p)
   (Hm : ¬ p ∣ m) (Hn : ¬ p ∣ n) : ¬ p ∣ m * n :=
 mt pp.dvd_mul.1 $ by simp [Hm, Hn]
 
+/-- Prime `p` divides the product of `L : list ℕ` iff it divides some `a ∈ L` -/
+lemma prime.dvd_prod_iff {p : ℕ} {L : list ℕ} (pp : p.prime) :
+  p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a :=
+begin
+  split,
+  { intros h,
+    induction L,
+    { simp only [list.prod_nil] at h, exact absurd h (prime.not_dvd_one pp) },
+    { rw list.prod_cons at h,
+      cases (prime.dvd_mul pp).mp h,
+      { use L_hd, simp [h_1] },
+      { rcases L_ih h_1 with ⟨x, hx1, hx2⟩, use x, simp [list.mem_cons_iff, hx1, hx2] } } },
+  { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (list.dvd_prod ha1) },
+end
+
+lemma prime.not_dvd_prod {p : ℕ} {L : list ℕ} (pp : prime p) (hL : ∀ a ∈ L, ¬ p ∣ a) :
+  ¬ p ∣ L.prod :=
+mt (prime.dvd_prod_iff pp).mp (not_bex.mpr hL)
+
 theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : prime p) (h : p ∣ m^n) : p ∣ m :=
 begin
   induction n with n IH,
@@ -641,16 +660,12 @@ section
 open list
 
 lemma mem_list_primes_of_dvd_prod {p : ℕ} (hp : prime p) :
-  ∀ {l : list ℕ}, (∀ p ∈ l, prime p) → p ∣ prod l → p ∈ l
-| []       := λ h₁ h₂, absurd h₂ (prime.not_dvd_one hp)
-| (q :: l) := λ h₁ h₂,
-  have h₃ : p ∣ q * prod l := @prod_cons _ _ l q ▸ h₂,
-  have hq : prime q := h₁ q (mem_cons_self _ _),
-  or.cases_on ((prime.dvd_mul hp).1 h₃)
-    (λ h, by rw [prime.dvd_iff_not_coprime hp, coprime_primes hp hq, ne.def, not_not] at h;
-      exact h ▸ mem_cons_self _ _)
-    (λ 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)))
+  ∀ {l : list ℕ}, (∀ p ∈ l, prime p) → p ∣ prod l → p ∈ l :=
+begin
+  intros L hL hpL,
+  rcases (prime.dvd_prod_iff hp).mp hpL with ⟨x, hx1, hx2⟩,
+  rwa ((prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2)
+end
 
 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,