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: prove Leibniz π series with Abel's limit theorem #11098

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: prove Leibniz π series with Abel's limit theorem #11098

wants to merge 8 commits into from

Conversation

Parcly-Taxel
Copy link
Collaborator

This resolves the Zulip comment here.

Open in Gitpod

@Parcly-Taxel Parcly-Taxel added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Mar 2, 2024
Parcly-Taxel and others added 2 commits March 3, 2024 16:56
@Parcly-Taxel @MichaelStollBayreuth
Update Mathlib/Topology/UniformSpace/Cauchy.lean
bbd56ac 
Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
@Parcly-Taxel
get rid of congr
0d0e40b
MichaelStollBayreuth
MichaelStollBayreuth approved these changes Mar 3, 2024
View reviewed changes
Copy link
Collaborator

@MichaelStollBayreuth MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

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

This looks good to me now, and I'll exercise my newly obtained powers to maintainer merge 😄

@MichaelStollBayreuth
Copy link
Collaborator

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 3, 2024

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

@sgouezel
Copy link
Contributor

sgouezel commented Mar 3, 2024

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Mar 3, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 3, 2024
@Parcly-Taxel
feat: prove Leibniz π series with Abel's limit theorem (#11098)
c021018 
This resolves the Zulip comment [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/416938975).
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 3, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: prove Leibniz π series with Abel's limit theorem [Merged by Bors] - feat: prove Leibniz π series with Abel's limit theorem Mar 3, 2024
@mathlib-bors mathlib-bors bot closed this Mar 3, 2024
@mathlib-bors mathlib-bors bot deleted the abelleibniz branch March 3, 2024 18:29
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@Parcly-Taxel @kbuzzard
feat: prove Leibniz π series with Abel's limit theorem (#11098)
f8c9ef3 
This resolves the Zulip comment [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/416938975).
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@Parcly-Taxel @dagurtomas
feat: prove Leibniz π series with Abel's limit theorem (#11098)
76bf21f 
This resolves the Zulip comment [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/416938975).
utensil pushed a commit that referenced this pull request Mar 26, 2024
@Parcly-Taxel @utensil
feat: prove Leibniz π series with Abel's limit theorem (#11098)
bab63dc 
This resolves the Zulip comment [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/416938975).
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@Parcly-Taxel @Louddy
feat: prove Leibniz π series with Abel's limit theorem (#11098)
368e888 
This resolves the Zulip comment [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Bounds.20on.20alternating.20convergent.20series/near/416938975).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth approved these changes

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Parcly-Taxel @MichaelStollBayreuth @sgouezel