mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

Modular forms

Open CBirkbeck opened this issue 4 years ago • 2 comments

Some files for defining modular forms and defining Eisenstein series. It also proves that Eisenstein series are modular forms. At the moment some are a complete mess, so still lots to do. Lots of this is based on work from Kevin Buzzard's birthday repo, so credit it due to other authors and I will try to find out who they are. Also note #10000 has been merged into this, so that is also not due to me.

Open in Gitpod

CBirkbeck avatar Sep 03 '21 15:09 CBirkbeck

  • [ ] depends on: #12393

CBirkbeck avatar Mar 02 '22 10:03 CBirkbeck

  • [ ] depends on: #13250

CBirkbeck avatar Apr 08 '22 18:04 CBirkbeck