Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-12 14:47 32d096dc

View on Github →

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.

Estimated changes

added theorem cusp_form.add_apply
added theorem cusp_form.coe_add
added theorem cusp_form.coe_neg
added theorem cusp_form.coe_smul
added theorem cusp_form.coe_sub
added theorem cusp_form.coe_zero
added theorem cusp_form.ext
added theorem cusp_form.neg_apply
added theorem cusp_form.smul_apply
added theorem cusp_form.sub_apply
added theorem cusp_form.zero_apply
added structure cusp_form
added theorem modular_form.add_apply
added theorem modular_form.coe_add
added theorem modular_form.coe_neg
added theorem modular_form.coe_smul
added theorem modular_form.coe_sub
added theorem modular_form.coe_zero
added theorem modular_form.ext
added def modular_form.mul
added theorem modular_form.mul_coe
added theorem modular_form.neg_apply
added theorem modular_form.sub_apply
added structure modular_form
modified theorem modular_form.mul_slash_SL2
modified theorem modular_form.neg_slash
modified theorem modular_form.slash_add
modified theorem modular_form.slash_one
modified theorem modular_form.smul_slash