Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(archive/100-theorems-list): add proof of thm 81 #7274

Closed
wants to merge 34 commits into from
Closed

[Merged by Bors] - feat(archive/100-theorems-list): add proof of thm 81 #7274

wants to merge 34 commits into from

Conversation

manuelcandales
Copy link
Collaborator

@manuelcandales manuelcandales commented Apr 20, 2021 •
edited by github-actions bot

@manuelcandales manuelcandales added the awaiting-review The author would like community review of the PR label Apr 20, 2021
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 20, 2021
@manuelcandales manuelcandales added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 20, 2021
@manuelcandales manuelcandales mentioned this pull request Apr 20, 2021
Closed
@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 21, 2021
benjamindavidson
benjamindavidson reviewed Apr 25, 2021
View reviewed changes
Copy link
Collaborator

@benjamindavidson benjamindavidson left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd love to review the actual content of this PR but unfortunately there's no cache. I suppose that is because the dependency tag prevented the branch from building? (though it wouldn't have passed the checks regardless)

archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean Outdated Show resolved Hide resolved
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 27, 2021
@manuelcandales manuelcandales added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 27, 2021
bors bot pushed a commit that referenced this pull request Apr 30, 2021
@manuelcandales
feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282)
46ac55a 
Every positive natural number can be expressed as m^2 * n where n is square free. Used in #7274
bors bot pushed a commit that referenced this pull request May 1, 2021
@manuelcandales
feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282)
d5d22c5 
Every positive natural number can be expressed as m^2 * n where n is square free. Used in #7274
@github-actions github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 1, 2021
@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-review The author would like community review of the PR label Mar 5, 2022
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 7, 2022
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 7, 2022
b-mehta
b-mehta approved these changes Mar 9, 2022
View reviewed changes
Copy link
Collaborator

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very minor suggestions from me, this is very nicely laid out!

Thanks for tagging me on this Eric - I do have a stronger version of this result in the unit-fractions project (giving the result that the sum up to x of prime reciprocals is log log x + b + O(1/log x)) but it uses a bunch of stuff not yet in mathlib, and the proof idea is pretty different. So I have no objection to this version being in the archive or in mathlib!

src/data/finset/card.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean Outdated Show resolved Hide resolved
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 11, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 12, 2022
@leanprover-community leanprover-community deleted a comment from github-actions bot Mar 12, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 12, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 12, 2022
@fpvandoorn
Copy link
Member

LGTM

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 18, 2022
bors bot pushed a commit that referenced this pull request Mar 18, 2022
@manuelcandales @Ruben-VandeVelde
feat(archive/100-theorems-list): add proof of thm 81 (#7274)
bf690dd 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(archive/100-theorems-list): add proof of thm 81 [Merged by Bors] - feat(archive/100-theorems-list): add proof of thm 81 Mar 18, 2022
@bors bors bot closed this Mar 18, 2022
@bors bors bot deleted the thm81 branch March 18, 2022 18:32
jjaassoonn pushed a commit that referenced this pull request Mar 21, 2022
@manuelcandales @Ruben-VandeVelde @jjaassoonn
feat(archive/100-theorems-list): add proof of thm 81 (#7274)
6050c86 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 left review comments

@hrmacbeth hrmacbeth hrmacbeth left review comments

@ericrbg ericrbg ericrbg left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@benjamindavidson benjamindavidson benjamindavidson left review comments

@b-mehta b-mehta b-mehta approved these changes

Assignees

@Ruben-VandeVelde Ruben-VandeVelde

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet