Skip to content

[Merged by Bors] - Eisenstein series are mdifferentiable#11013

Closed
CBirkbeck wants to merge 170 commits intomasterfrom
eisensteinSeries_MDifferentiable
Closed

[Merged by Bors] - Eisenstein series are mdifferentiable#11013
CBirkbeck wants to merge 170 commits intomasterfrom
eisensteinSeries_MDifferentiable

Conversation

@CBirkbeck
Copy link
Copy Markdown
Collaborator

@CBirkbeck CBirkbeck commented Feb 27, 2024

CBirkbeck and others added 30 commits February 6, 2024 17:48
…mposition.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…mposition.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ergence.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@CBirkbeck CBirkbeck added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2024
@loefflerd
Copy link
Copy Markdown
Contributor

Looks good to me now. If you're happy with it, please label with "awaiting review" and "awaiting CI", and I'll flag it for merging if the CI run passes.

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 27, 2024
@CBirkbeck CBirkbeck added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 27, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2024
@CBirkbeck
Copy link
Copy Markdown
Collaborator Author

done!

@loefflerd
Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions
Copy link
Copy Markdown

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 27, 2024
@RemyDegenne
Copy link
Copy Markdown
Contributor

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 27, 2024
We show that Eisenstein Series are MDifferentiable

- [x] depends on: #10377 
- [x] depends on:  #11244



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title Eisenstein series are mdifferentiable [Merged by Bors] - Eisenstein series are mdifferentiable May 27, 2024
@mathlib-bors mathlib-bors bot closed this May 27, 2024
@mathlib-bors mathlib-bors bot deleted the eisensteinSeries_MDifferentiable branch May 27, 2024 15:31
callesonne pushed a commit that referenced this pull request Jun 4, 2024
We show that Eisenstein Series are MDifferentiable

- [x] depends on: #10377 
- [x] depends on:  #11244



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
js2357 pushed a commit that referenced this pull request Jun 18, 2024
We show that Eisenstein Series are MDifferentiable

- [x] depends on: #10377 
- [x] depends on:  #11244



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

7 participants