[Merged by Bors] - feat: Eisenstein q exp identity

[CBirkbeck]

We prove that Eisenstein series have a q-expansion of the form 1 - (2k / bernoulli k) ∑' n, σ_{k-1}(n) q^n

---

• depends on: [Merged by Bors] - Iterated derivatives of tsum's within some open set. #26016
• depends on: [Merged by Bors] - feat(Analysis/SpecialFunctions): iterated derivative of cotangent #27212
• depends on: [Merged by Bors] - feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. #27837
• depends on: [Merged by Bors] - feat: normalised Eisenstein series #27839
• depends on: [Merged by Bors] - feat(NumberTheory/ModularForms/EisensteinSeries): Update gammaSet #27840
• depends on: [Merged by Bors] - feat(NumberTheory/Divisors): divisors antidiagonal tsum #28690
• depends on: feat(NumberTheory/LSeries/RiemannZeta): add tsum over ints lemma. #27838
• depends on: [Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas #27841
• depends on: [Merged by Bors] - Add q-expansion identities for Eisenstein series. #27844

[MichaelStollBayreuth]

LGTM now.
maintainer merge

[github-actions]

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

[riccardobrasca]

Can you add at least the main declaration of this PR to the doc at the beginning of the file? Thanks!

bors d+

[mathlib-bors]

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

bors r+

[bryangingechen]

Just requeueing with a title that fits our conventions better.
bors r-
bors r+

[mathlib-bors]

Canceled.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step

[leanprover-radar]

Benchmarking c38fcdb (status) against 472dcfc (status).

_{React with 👀 to be notified when the results are in. The command author is always notified.}