Prime dividing a product

Stream: Is there code for X?

[Yaël Dillies]

Do we have that if a prime divides a finset.prodthen it divides one of the factors?

lemma exists_mem_finset_dvd {ι : Sort*} [decidable_eq ι] {p : α} (hp : prime p) {s : finset ι}
  {f : ι → α} :
  p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=

A close match is exists_mem_multiset_dvd_of_prime.

[Floris van Doorn]

Looks like we don't have it, but the match is indeed very close:

import algebra.associated
import algebra.big_operators.basic

lemma exists_mem_finset_dvd {ι : Sort*} {α : Type*} [comm_monoid_with_zero α] [decidable_eq ι]
  {p : α} (hp : prime p) {s : finset ι} {f : ι → α} (h : p ∣ s.prod f) : ∃ i ∈ s, p ∣ f i :=
by { convert exists_mem_multiset_dvd_of_prime hp h, simp [finset.mem_def] }

[Yaël Dillies]

Eheh, you beat me on this one

lemma exists_mem_finset_dvd {ι : Sort*} [decidable_eq ι] {p : α} (hp : prime p) {s : finset ι}
  {f : ι → α} :
  p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=
finset.induction_on s (λ h, (hp.not_dvd_one $ finset.prod_empty.subst h).elim) $
λ i s hi ih h,
begin
  obtain hpf | hps := hp.dvd_or_dvd ((finset.prod_insert hi).subst h),
  { exact ⟨i, finset.mem_insert_self i s, hpf⟩ },
  { obtain ⟨j, hj, hpf⟩ := ih hps,
    exact ⟨j, finset.mem_insert_of_mem hj, hpf⟩ }
end