# Zulip Chat Archive

## 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?

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

(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