feat(algebra/big_operators/finprod): add finprod.mem_dvd (#9549)

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

src/algebra/big_operators/basic.lean

@@ -1044,6 +1044,14 @@ lemma _root_.fintype.prod_eq_prod_compl_mul [decidable_eq α] [fintype α] (a :
   ∏ i, f i = (∏ i in {a}ᶜ, f i) * f a :=
 prod_eq_prod_diff_singleton_mul (mem_univ a) f
 
+lemma dvd_prod_of_mem (f : α → β) {a : α} {s : finset α} (ha : a ∈ s) :
+  f a ∣ ∏ i in s, f i :=
+begin
+  classical,
+  rw finset.prod_eq_mul_prod_diff_singleton ha,
+  exact dvd_mul_right _ _,
+end
+
 /-- A product can be partitioned into a product of products, each equivalent under a setoid. -/
 @[to_additive "A sum can be partitioned into a sum of sums, each equivalent under a setoid."]
 lemma prod_partition (R : setoid α) [decidable_rel R.r] :

src/algebra/big_operators/finprod.lean

@@ -566,6 +566,18 @@ end
   ∏ᶠ i ∈ (insert a s), f i = ∏ᶠ i ∈ s, f i :=
 finprod_mem_insert_of_eq_one_if_not_mem (λ _, h)
 
+/-- If the multiplicative support of `f` is finite, then for every `x` in the domain of `f`,
+`f x` divides `finprod f`.  -/
+lemma finprod_mem_dvd {f : α → N} (a : α) (hf : finite (mul_support f)) :
+  f a ∣ finprod f :=
+begin
+  by_cases ha : a ∈ mul_support f,
+  { rw finprod_eq_prod_of_mul_support_to_finset_subset f hf (set.subset.refl _),
+    exact finset.dvd_prod_of_mem f ((finite.mem_to_finset hf).mpr ha) },
+  { rw nmem_mul_support.mp ha,
+    exact one_dvd (finprod f) }
+end
+
 /-- The product of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a * f b`. -/
 @[to_additive] lemma finprod_mem_pair (h : a ≠ b) : ∏ᶠ i ∈ ({a, b} : set α), f i = f a * f b :=
 by { rw [finprod_mem_insert, finprod_mem_singleton], exacts [h, finite_singleton b] }