Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

add file containing the Weierstrass M-test #8981

Closed
wants to merge 1 commit into from
Closed

add file containing the Weierstrass M-test #8981

wants to merge 1 commit into from

Conversation

CBirkbeck
Copy link
Collaborator

Open in Gitpod

@CBirkbeck CBirkbeck added the awaiting-review The author would like community review of the PR label Sep 3, 2021
@hrmacbeth
Copy link
Member

I sketch an alternative approach at
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Modular.20forms.20and.20related.20things/near/252246795
Let's discuss at that link, and close this PR if the alternative approach is adopted.

@CBirkbeck
Copy link
Collaborator Author

I sketch an alternative approach at
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Modular.20forms.20and.20related.20things/near/252246795
Let's discuss at that link, and close this PR if the alternative approach is adopted.

Yes that sounds good. I'm happy to close this in favour of something better! Thank you.

@CBirkbeck CBirkbeck added incomplete and removed awaiting-review The author would like community review of the PR labels Sep 7, 2021
@YaelDillies YaelDillies added the t-analysis Analysis (normed *, calculus) label Apr 19, 2023
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@CBirkbeck CBirkbeck closed this May 28, 2024
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
incomplete t-analysis Analysis (normed *, calculus) too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@CBirkbeck @hrmacbeth @kim-em @YaelDillies