Skip to content

Dedekind eta e2#28596

Closed
CBirkbeck wants to merge 154 commits intoleanprover-community:masterfrom
CBirkbeck:Dedekind_eta_E2
Closed

Dedekind eta e2#28596
CBirkbeck wants to merge 154 commits intoleanprover-community:masterfrom
CBirkbeck:Dedekind_eta_E2

Conversation

@CBirkbeck
Copy link
Copy Markdown
Collaborator

@CBirkbeck CBirkbeck commented Aug 18, 2025 •
edited
Loading

We show that the logarithmic derivative of the Dedekind eta function equals the the Eisenstein series E2 (up to a constant).

Open in Gitpod

CBirkbeck added 30 commits May 12, 2025 21:41
@CBirkbeck
Eisenstein E2
130bd35
@CBirkbeck
save
3659155
@CBirkbeck
save
7ac9441
@CBirkbeck
save
e761796
@CBirkbeck
feat(Analysis/NormedSpace/FunctionSeries): Add SummableUniformlyOn ve…
d53f78e 
…rsions and derivwithin_tsum
@CBirkbeck
update
9a0f6cc
@CBirkbeck
Merge remote-tracking branch 'origin/master' into CB_Eisenstein_E2
23902bd
@CBirkbeck
Merge remote-tracking branch 'origin/master' into derivwithin_tsum
89ad73f
@CBirkbeck
mk_all
4102288
@CBirkbeck
Merge branch 'CB_Eisenstein_E2' of https://github.com/CBirkbeck/mathlib4
8cebcb8 
 into CB_Eisenstein_E2
@CBirkbeck
Merge remote-tracking branch 'origin/master' into derivwithin_tsum
d4df7b6
@CBirkbeck
move files
7311794
@CBirkbeck
imports
2f47769
@CBirkbeck
mk_all
5a4f0f3
@CBirkbeck
fix name
da64063
@CBirkbeck
fix name
8802150
@CBirkbeck
name fix again
f78e869
@CBirkbeck
fix
991df02
@CBirkbeck
merge
5311723
@CBirkbeck
updates
aaf9ca4
@CBirkbeck
updates
612c83a
@CBirkbeck
updates2
9a292d7
@CBirkbeck
fix build
141652a
@CBirkbeck
fix
89406e3
@CBirkbeck
Add itereatedDerivWithin version of zpow lemmas
8f1c4a3
@CBirkbeck
add file!
df2bf4a
@CBirkbeck
fix build
217237c
@CBirkbeck
open
db2fc70
@CBirkbeck
add content
17a3282
@CBirkbeck
space
96a4c69
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 21, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 21, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 25, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 25, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 27, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 28, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Jan 21, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 5, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 5, 2026

This pull request has conflicts, please merge master and resolve them.

@CBirkbeck CBirkbeck closed this Feb 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@CBirkbeck @mathlib4-dependent-issues-bot @mathlib4-merge-conflict-bot @mbkybky @themathqueen
⚡