feat(archive/100-theorems-list): perfect numbers (nr 70)

[awainverse]

Defining perfect numbers, proving the Euclid-Euler theorem (Theorem 70)

---

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfect.20Numbers/near/201098280

[jcommelin]

Some general comments on style (to make the code in mathlib look uniform):
A typical lemma is formatted as

lemma some_name (h : hypothesis) :
  statement indented by 2 spaces :=
begin
  split, -- inside begin..end indent by 2
  { tactic1,
    tactic2 }, -- closing brace on same line as last tactic
  { etc }
end

[awainverse]

I made fundamental changes to the proof, in a new version which lives in src/multiplicity_vectors.lean and archive/100-theorems-list/pnat_perfect.lean. I have some other ideas (with sorries) not actually necessary for this proof at src/divisibility_lattice.lean.

I think I'm basically happy with the approach in pnat_perfect.lean, so I will mark as resolved any comments that are resolved in that file, and will eventually replace the original file if people agree it's as good.

I'd also like advice on how to break up this PR and where to put the contents of multiplicity_vectors.lean.

[jcommelin]

A first set of comments.

[jcommelin]

I don't think that we want this to be the global has_inf instance for finsupps. I guess you can replace nat with a certain type of lattice X and deduce some other lattice structure for \a →\0 X.
I haven't checked how much of this is already done in the library.

[jcommelin]

There should already be a pnat.coe_inj or something like that.

[awainverse]

There is pnat.eq, but I rewrite the other way several times, and feed it into simp.

[jcommelin]

This section looks really good to me. It can be PRd to data/pnat/*.
I think all of it can go in xgcd.lean in that directory, but if you find better places, go ahead.

[awainverse]

#3274

[jcommelin]

@awainverse Small tip: if you are done with a review comment, please click "resolve conversation" to mark it as done. That way others can quickly see what's done and what needs attention.

[sgouezel]

If this is ready for review, can you change the label "changes requested" to "request review"? Otherwise, can you say what remains to be done on your side?

[bryangingechen]

What's the status of this PR now? #3291 was closed without being merged. Is there another (future) PR that this depends on?

[awainverse]

I've marked this as WIP. I'm working on refactoring unique factorization in general, and I think that'll make factorization for nats nicer, allowing me to make this proof very clean. I can close the PR or revisit it and try to make it work without the new API if you think that'd be better.

[bryangingechen]

Thanks for the update! I'm happy to leave this open until the new API is ready.

[jcommelin]

@awainverse What's the status now? It's not clear to me whether you want to resurrect this PR, or want to build a new one...