Commit 2026-08-03 00:07 9c0c555b

View on Github →

feat(NumberTheory): use IsApply for ModularForm etc (#41561) We use IsApply classes for SlashInvariantForm, ModularForm and CuspForm at the same time to avoid temporary name clashes and since they are not used as widely as LinearMap and ContinuousLinearMap for example.

Estimated changes

deleted theorem CuspForm.IsGLPos.coe_smul
deleted theorem CuspForm.add_apply
deleted def CuspForm.coeHom
deleted theorem CuspForm.coe_add
deleted theorem CuspForm.coe_neg
deleted theorem CuspForm.coe_smul
deleted theorem CuspForm.coe_sub
deleted theorem CuspForm.coe_zero
deleted theorem CuspForm.neg_apply
deleted theorem CuspForm.smul_apply
deleted theorem CuspForm.sub_apply
deleted theorem CuspForm.zero_apply
deleted theorem ModularForm.add_apply
deleted def ModularForm.coeHom
deleted theorem ModularForm.coe_add
deleted theorem ModularForm.coe_neg
deleted theorem ModularForm.coe_smul
deleted theorem ModularForm.coe_sub
deleted theorem ModularForm.coe_zero
deleted theorem ModularForm.neg_apply
deleted theorem ModularForm.smul_apply
deleted theorem ModularForm.sub_apply
deleted theorem ModularForm.zero_apply