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): Sum of the Reciprocals of the Triangular Numbers #2692

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers #2692

wants to merge 17 commits into from

Conversation

jalex-stark
Copy link
Collaborator

@jalex-stark jalex-stark commented May 15, 2020 •
edited

Adds a folder archive/100-theorems-list, moves our proof of 82 into it, and provides a proof of 42. There's a readme, I haven't really thought about what should go in there.

@bryangingechen bryangingechen changed the title Freek 42 feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers May 15, 2020
digama0
digama0 previously requested changes May 15, 2020
View reviewed changes
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/inverse-triangle-sum.lean Outdated Show resolved Hide resolved
@bryangingechen
Copy link
Collaborator

Do you mind adding numbers at the start of the filenames? I think the consensus on Zulip was that this was a good idea.

Regarding the contents of the README, I think we can come back and edit it after the 100 theorems page on the community website takes shape.

@urkud
Copy link
Member

urkud commented May 16, 2020

I simplified some proofs and added a multiplicative version of sum_range_induction.

@urkud urkud requested a review from digama0 May 16, 2020 09:39
bryangingechen
bryangingechen reviewed May 16, 2020
View reviewed changes
src/algebra/big_operators.lean Outdated Show resolved Hide resolved
src/algebra/big_operators.lean Outdated Show resolved Hide resolved
archive/100-theorems-list/42_inverse_triangle_sum.lean Outdated Show resolved Hide resolved
@rwbarton
Copy link
Collaborator

Adds a folder archive/100-theorems-list, moves our proof of 82 into it, and provides a proof of 42.

As a general rule of thumb, if you use "and" to describe what a PR does, it probably does too many things. It would be better to have a separate PR which just performs the reorganization.

@urkud @bryangingechen @jalex-stark
Apply suggestions from code review
58ea0e1 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Jalex Stark <alexmaplegm@gmail.com>
@jalex-stark
Copy link
Collaborator Author

As a general rule of thumb, if you use "and" to describe what a PR does, it probably does too many things. It would be better to have a separate PR which just performs the reorganization.

Do you think it's worthwhile to split this PR up right now?

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label May 17, 2020
@bryangingechen bryangingechen dismissed digama0’s stale review May 17, 2020 02:03

comments have been addressed

@bryangingechen
Copy link
Collaborator

LGTM, thank you!
bors r+

@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 May 17, 2020
bors bot pushed a commit that referenced this pull request May 17, 2020
@jalex-stark @urkud
feat(archive/100-theorems-list): Sum of the Reciprocals of the Triang…
4f484a1 
…ular Numbers (#2692)

Adds a folder `archive/100-theorems-list`, moves our proof of 82 into it, and provides a proof of 42. There's a readme, I haven't really thought about what should go in there.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented May 17, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers [Merged by Bors] - feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers May 17, 2020
@bors bors bot closed this May 17, 2020
@bors bors bot deleted the freek-42 branch May 17, 2020 04:33
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@jalex-stark @urkud @cipher1024
feat(archive/100-theorems-list): Sum of the Reciprocals of the Triang…
195bdfd 
…ular Numbers (leanprover-community#2692)

Adds a folder `archive/100-theorems-list`, moves our proof of 82 into it, and provides a proof of 42. There's a readme, I haven't really thought about what should go in there.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@jcommelin jcommelin jcommelin left review comments

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
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
6 participants
@jalex-stark @bryangingechen @urkud @rwbarton @digama0 @jcommelin