## Stream: new members

### Topic: Where to PR a proof?

#### Stuart Presnell (Dec 08 2021 at 18:58):

I've PR'ed a proof (#10624) of a generalisation of prime.dvd_mul for the product of a list ℕ. I'm wondering if it would be useful to also PR my proofs of the corresponding statements for finset and finsupp:

lemma finset.dvd_prod {p : ℕ} {S : finset ℕ} (pp : prime p) (g : ℕ → ℕ) :
p ∣ S.prod g ↔ ∃ (a : ℕ) (H : a ∈ S), p ∣ g a :=


and

lemma finsupp.dvd_prod {p : ℕ} {f: ℕ →₀ ℕ} (pp : prime p) :
(p ∣ f.prod pow) ↔ ∃ a ∈ f.support, p ∣ a^(f a) :=


#### Stuart Presnell (Dec 08 2021 at 18:59):

If so, where should these proofs go? For example, no file in data/finset seems to know about prime, while data/nat/prime doesn't know about finset.prod.

#### Mario Carneiro (Dec 08 2021 at 18:59):

those look like algebra.big_operators

#### Johan Commelin (Dec 08 2021 at 19:00):

Maybe algebra/big_operators/prime.lean?

#### Johan Commelin (Dec 08 2021 at 19:00):

If it doesn't exist yet, feel free to start it

#### Stuart Presnell (Dec 08 2021 at 19:01):

It doesn't, so I shall. Thanks very much.

#### Stuart Presnell (Dec 08 2021 at 19:03):

More generally, if you have a proof that involves definitions/theorems X and Y, is there a general method to determine which files know about both of them?

#### Andrew Yang (Dec 08 2021 at 19:07):

You might find this python script helpful.
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Finding.20homes.20for.20lemmas/near/260255746

#### Eric Rodriguez (Dec 08 2021 at 19:10):

for finsupp.dvd_prod, can't it be p \| a? also you can probably generalize this to some level of monoid

#### Johan Commelin (Dec 08 2021 at 19:17):

Well, there is always the nat.prime vs prime issue. I guess these lemmas should be called something like nat.prime.dvd_prod_iff

#### Stuart Presnell (Dec 08 2021 at 19:56):

Thanks all for your help. PR'ed as #10675

#### Stuart Presnell (Dec 08 2021 at 20:01):

I wasn't sure how the various nat, prime and finset/finsupp prefixes should stack up. From the root namespace is there a standard order in which these should go? That is, should these be nat.prime.finset.dvd_prod_iff or finset.nat.prime.dvd_prod_iff or something else?

(deleted)

#### Yaël Dillies (Dec 08 2021 at 20:07):

You shouldn't literally stack namespaces

#### Stuart Presnell (Dec 08 2021 at 20:08):

No, I've put the two lemmas in separate namespaces finset and finsupp.

#### Stuart Presnell (Dec 08 2021 at 20:09):

Within these, should each lemma then be called nat.prime.dvd_prod_iff?

#### Yaël Dillies (Dec 08 2021 at 20:09):

In that case, you have an hypothesis of type nat.prime, so you should start with nat.prime for dot notation to work. Then it depends on the specific convention. Here I would do something like nat.prime.dvd_finset_prod_iff

#### Yaël Dillies (Dec 08 2021 at 20:10):

Yeah, that's precisely what I don't want you to do. You (usually) shouldn't have something like nat.prime.finset or finset.nat.prime.

#### Stuart Presnell (Dec 08 2021 at 20:11):

Ok, I'll get rid of the namespaces and rename them as you suggested.

Last updated: Dec 20 2023 at 11:08 UTC