feat(algebra/big_operators/associated): generalize prod_primes_dvd (#…

…12740)

src/algebra/big_operators/associated.lean

@@ -64,6 +64,45 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
   end)
 
+lemma multiset.prod_primes_dvd
+  [cancel_comm_monoid_with_zero α] [Π a : α, decidable_pred (associated a)]
+  {s : multiset α} (n : α) (h : ∀ a ∈ s, prime a) (div : ∀ a ∈ s, a ∣ n)
+  (uniq : ∀ a, s.countp (associated a) ≤ 1) :
+  s.prod ∣ n :=
+begin
+  induction s using multiset.induction_on with a s induct n primes divs generalizing n,
+  { simp only [multiset.prod_zero, one_dvd] },
+  { rw multiset.prod_cons,
+    obtain ⟨k, rfl⟩ : a ∣ n := div a (multiset.mem_cons_self a s),
+    apply mul_dvd_mul_left a,
+    refine induct
+      (λ a ha, h a (multiset.mem_cons_of_mem ha))
+      (λ a, (multiset.countp_le_of_le _ (multiset.le_cons_self _ _)).trans (uniq a))
+      k (λ b b_in_s, _),
+    { have b_div_n := div b (multiset.mem_cons_of_mem b_in_s),
+      have a_prime := h a (multiset.mem_cons_self a s),
+      have b_prime := h b (multiset.mem_cons_of_mem b_in_s),
+      refine (b_prime.dvd_or_dvd b_div_n).resolve_left (λ b_div_a, _),
+      have assoc := b_prime.associated_of_dvd a_prime b_div_a,
+      have := uniq a,
+      rw [multiset.countp_cons_of_pos _ (associated.refl _), nat.succ_le_succ_iff, ←not_lt,
+        multiset.countp_pos] at this,
+      exact this ⟨b, b_in_s, assoc.symm⟩ } }
+end
+
+lemma finset.prod_primes_dvd
+  [cancel_comm_monoid_with_zero α] [unique αˣ]
+  {s : finset α} (n : α) (h : ∀ a ∈ s, prime a) (div : ∀ a ∈ s, a ∣ n) :
+  (∏ p in s, p) ∣ n :=
+begin
+  classical,
+  exact multiset.prod_primes_dvd n
+    (by simpa only [multiset.map_id', finset.mem_def] using h)
+    (by simpa only [multiset.map_id', finset.mem_def] using div)
+    (by simp only [multiset.map_id', associated_eq_eq, multiset.countp_eq_card_filter,
+        ←multiset.count_eq_card_filter_eq, ←multiset.nodup_iff_count_le_one, s.nodup]),
+end
+
 namespace associates
 
 section comm_monoid

src/number_theory/primorial.lean

@@ -3,9 +3,10 @@ Copyright (c) 2020 Patrick Stevens. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Stevens
 -/
-import tactic.ring_exp
-import data.nat.parity
+import algebra.big_operators.associated
 import data.nat.choose.sum
+import data.nat.parity
+import tactic.ring_exp
 
 /-!
 # Primorial
@@ -60,27 +61,6 @@ begin
   exacts [(s h).elim, (t h).elim],
 end
 
-lemma prod_primes_dvd {s : finset ℕ} : ∀ (n : ℕ) (h : ∀ a ∈ s, nat.prime a) (div : ∀ a ∈ s, a ∣ n),
-  (∏ p in s, p) ∣ n :=
-begin
-  apply finset.induction_on s,
-  { simp, },
-  { intros a s a_not_in_s induct n primes divs,
-    rw finset.prod_insert a_not_in_s,
-    obtain ⟨k, rfl⟩ : a ∣ n := divs a (finset.mem_insert_self a s),
-    apply mul_dvd_mul_left a,
-    apply induct k,
-    { intros b b_in_s,
-      exact primes b (finset.mem_insert_of_mem b_in_s), },
-    { intros b b_in_s,
-      have b_div_n := divs b (finset.mem_insert_of_mem b_in_s),
-      have a_prime := primes a (finset.mem_insert_self a s),
-      have b_prime := primes b (finset.mem_insert_of_mem b_in_s),
-      refine ((prime.dvd_mul b_prime).mp b_div_n).resolve_left (λ b_div_a, _),
-      obtain rfl : b = a := ((nat.dvd_prime a_prime).1 b_div_a).resolve_left b_prime.ne_one,
-      exact a_not_in_s b_in_s, } },
-end
-
 lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
 | 0 := le_rfl
 | 1 := le_of_inf_eq rfl
@@ -119,7 +99,7 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
                 have s : ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)),
                   i ∣ choose (2 * m + 1) (m + 1),
                 { refine prod_primes_dvd  (choose (2 * m + 1) (m + 1)) _ _,
-                  { intros a, rw finset.mem_filter, apply and.right, },
+                  { intros a, rw [finset.mem_filter, nat.prime_iff], apply and.right, },
                   { intros a, rw finset.mem_filter,
                     intros pr,
                     rcases pr with ⟨ size, is_prime ⟩,