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 :=


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.

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):


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