Where to PR a proof?

Stream: new members

[Stuart Presnell]

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]

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]

those look like algebra.big_operators

[Johan Commelin]

Maybe algebra/big_operators/prime.lean?

[Johan Commelin]

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

[Stuart Presnell]

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

[Stuart Presnell]

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]

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

[Eric Rodriguez]

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

[Johan Commelin]

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]

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

[Stuart Presnell]

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]

(deleted)

[Yaël Dillies]

You shouldn't literally stack namespaces

[Stuart Presnell]

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

[Stuart Presnell]

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

[Yaël Dillies]

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]

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]

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