Commit 2026-02-12 19:30 6c7376c4

View on Github →

feat(NumberTheory/ModularForms): remove unnecessary instance arguments (#35169) Adjust proof of isCusp_of_mem_strictPeriods to get rid of two unnecessary instance arguments.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

modified theorem Subgroup.isCusp_of_mem_strictPeriods

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

modified theorem CuspFormClass.exp_decay_atImInfty'

modified theorem ModularFormClass.analyticAt_cuspFunction_zero

modified theorem ModularFormClass.cuspFunction_apply_zero

modified theorem ModularFormClass.differentiableAt_cuspFunction

modified theorem ModularFormClass.differentiableOn_cuspFunction_ball

modified theorem ModularFormClass.exp_decay_sub_atImInfty

modified theorem ModularFormClass.hasFPowerSeries_cuspFunction

modified theorem ModularFormClass.hasSum_qExpansion

modified theorem ModularFormClass.hasSum_qExpansion_of_norm_lt

modified theorem ModularFormClass.qExpansionFormalMultilinearSeries_radius

modified theorem ModularFormClass.qExpansion_coeff_eq_circleIntegral

modified theorem ModularFormClass.qExpansion_coeff_eq_intervalIntegral

modified theorem ModularFormClass.qExpansion_coeff_zero

modified theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty