mathlib

32d096dc - feat(number_theory/modular_forms): Modular form definition (#13250)

feat(number_theory/modular_forms): Modular form definition (#13250) This contains the basic definitions of modular forms and cusp forms together with some basic lemmas. Co-authored-by: Johan Commelin <johan@commelin.net>