Commit 2023-07-03 16:47 ef8a6a92

View on Github →

feat: port NumberTheory.ModularForms.Basic (#5662)

Estimated changes

added theorem CuspForm.add_apply
added def CuspForm.coeHom
added theorem CuspForm.coe_add
added theorem CuspForm.coe_neg
added theorem CuspForm.coe_smul
added theorem CuspForm.coe_sub
added theorem CuspForm.coe_zero
added theorem CuspForm.ext
added theorem CuspForm.neg_apply
added theorem CuspForm.smul_apply
added theorem CuspForm.sub_apply
added theorem CuspForm.toFun_eq_coe
added theorem CuspForm.zero_apply
added structure CuspForm
added theorem ModularForm.add_apply
added theorem ModularForm.coe_add
added theorem ModularForm.coe_neg
added theorem ModularForm.coe_smul
added theorem ModularForm.coe_sub
added theorem ModularForm.coe_zero
added theorem ModularForm.ext
added def ModularForm.mul
added theorem ModularForm.mul_coe
added theorem ModularForm.neg_apply
added theorem ModularForm.smul_apply
added theorem ModularForm.sub_apply
added theorem ModularForm.zero_apply
added structure ModularForm
added theorem SlashInvariantForm.ext
deleted theorem slashInvariantForm_ext