-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(archive/100-theorems-list/70_perfect_numbers): Perfect Number Theorem, Direction 2 #4621
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you please add the result to 100.yaml
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…eorem, Direction 2 (#4621) Adds a few extra lemmas about `divisors`, `proper_divisors` and sums of proper divisors Proves Euler's direction of the Perfect Number theorem, finishing Freek 70
Canceled. |
bors r+ |
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
…eorem, Direction 2 (#4621) Adds a few extra lemmas about `divisors`, `proper_divisors` and sums of proper divisors Proves Euler's direction of the Perfect Number theorem, finishing Freek 70
Canceled. |
I'm pretty sure that it'll build now that I've set up a link to the archive instead of a Perhaps we could have a separate conversation about whether we want to move this stuff into |
@@ -224,7 +224,8 @@ | |||
author : mathlib | |||
70: | |||
title : The Perfect Number Theorem | |||
decl : nat.even_and_perfect_iff | |||
links : | |||
mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/70_perfect_numbers.lean |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@bryangingechen what is the correct way of linking here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It works now, and at least one other Freek problem has this form, so I'll tell bors to merge.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think it makes sense to move this to src/.
As far as I know, there are not really any other applications of perfect numbers, so far. So leaving it in the archive seems fine for now.
bors r+ |
…eorem, Direction 2 (#4621) Adds a few extra lemmas about `divisors`, `proper_divisors` and sums of proper divisors Proves Euler's direction of the Perfect Number theorem, finishing Freek 70
Pull request successfully merged into master. Build succeeded: |
Adds a few extra lemmas about
divisors
,proper_divisors
and sums of proper divisorsProves Euler's direction of the Perfect Number theorem, finishing Freek 70