[Merged by Bors] - Eisenstein series are modular forms#12604
[Merged by Bors] - Eisenstein series are modular forms#12604
Conversation
…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>
…y' into eisensteinSeries_are_mod_forms
|
This PR/issue depends on:
|
PR summary 255342ca38Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
riccardobrasca
left a comment
There was a problem hiding this comment.
Can you add a TODO to prove that it is not zero? Thanks!
bors d+
Mathlib/NumberTheory/ModularForms/EisensteinSeries/ModularForm.lean
Outdated
Show resolved
Hide resolved
|
|
||
| /-- This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence | ||
| condition given by `a: Fin 2 → ZMod N`. -/ | ||
| def eisensteinSeries_MF {k : ℤ} {N : ℕ+} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : |
There was a problem hiding this comment.
The name EisensteinSeries.eisensteinSeries_MF seems weird. Maybe ModularForms.eisensteinSeries?
There was a problem hiding this comment.
Hmm good point, we actually already have EinsesteinSeries.eisensteinSeries which seems like a bad thing. I might put this in the root namespace and then make the other one ModularForms.eisensteinSeries_MF to denote its a mod form. Does that sound ok?
|
✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with |
|
As for the TODO, I already have this, but its waiting on the q-expansion stuff thats coming. Should that still be a todo if its in the process of being PRd? |
I would do so - the next PR can remove the TODO. If that other PR doesn't land soon (for whatever reason), the current file is in a more useful state. |
|
bors r+ |
We show Eisenstein series are modular forms. Co-authored-by: Chris Birkbeck <c.birkbeck@ucl.ac.uk>
|
Pull request successfully merged into master. Build succeeded: |
We show Eisenstein series are modular forms.