Divisibility of big product over Finsets

Stream: general

[Adam Kurkiewicz]

Hi all, I'm working on Compfiles IMO 1970 P4

I'm still learning about Finset API and relevant tactics.

I would like to show that if a prime number divides a product of all natural numebrs in a Finset , then it also divides one natural number in a Finset.

I found a proof in Mathlib, which is almost exactly what I need, and it works with some kind of abstract definition of primality, but it doesn't work with a normal definition of primality:

This works:

import Mathlib.Tactic

theorem prime_dvd_elem_of (p : ℕ) (pp : Prime p) (s : Finset ℕ) : p ∣ (∏ m ∈ s, m) → ∃ x ∈ s, p ∣ x := by
  exact Prime.exists_mem_finset_dvd pp

But this doesn't:

import Mathlib.Tactic

theorem prime_dvd_elem_of (p : ℕ) (pp : Nat.Prime p) (s : Finset ℕ) : p ∣ (∏ m ∈ s, m) → ∃ x ∈ s, p ∣ x := by
  exact Prime.exists_mem_finset_dvd pp

Is there a different lemma I should use?

[Riccardo Brasca]

Just use Nat.prime_iff to connect the two notions.

[Adam Kurkiewicz]

Perfect, thank you!

[Riccardo Brasca]

Note that you can use dot notation nicely: if pp : Nat.Prime p then pp.Prime : Prime p (this is why we have Nat.Prime.prime as a separate lemma)

[Adam Kurkiewicz]

Oh yes, that's very nice

[Yaël Dillies]

Typo: It should be pp.prime : Prime p

[Adam Kurkiewicz]

I've worked out this much :)