This repository consists of Lean code which defines modular forms and looks to prove that Eisenstein series satisfy these definitions.
The code within is being organised in order to be added to mathlib.
Most of the code in the master brance is sorry free, other than the modularity conjecture and on going work on q-expansions of Eisenstein series.
In order to use this repository follow the instructions here: https://leanprover-community.github.io/leanproject.html using the files in this repository. In other words, after installing lean run leanproject get https://github.com/CBirkbeck/ModularForms.git.