Commit 2026-02-16 13:52 bb5c5a5a

View on Github →

feat(NumberTheory/ModularForms/QExpansion): define qExpansion ring hom and some more API (#32959) We construct the ring homomorphism from the graded ring of modular forms to power series. We develop some basic API for this and also prove the qExpansion coefficients are unique, which is useful to extracting the actual qExpansions of Eisenstein series.

Estimated changes

Modified Mathlib/Analysis/Complex/Periodic.lean

added theorem Function.Periodic.cuspFunction_add

added theorem Function.Periodic.cuspFunction_neg

added theorem Function.Periodic.cuspFunction_smul

added theorem Function.Periodic.cuspFunction_sub

added theorem Function.Periodic.tendsto_nhds_zero

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

modified def ModularFormClass.qExpansion

added theorem ModularFormClass.qExpansionFormalMultilinearSeries_coeff

modified theorem ModularFormClass.qExpansion_coeff

added theorem cuspFunction_add

added theorem cuspFunction_mul

added theorem cuspFunction_mul_zero

added theorem cuspFunction_neg

added theorem cuspFunction_smul

added theorem cuspFunction_sub

added theorem hasFPowerSeriesOnBall_cuspFunction

added def qExpansionAddHom

added def qExpansionRingHom

added theorem qExpansionRingHom_apply

added theorem qExpansion_add

added theorem qExpansion_coeff_unique

added theorem qExpansion_eq_zero_iff

added theorem qExpansion_mul

added theorem qExpansion_mul_coeff_zero

added theorem qExpansion_neg

added theorem qExpansion_of_mul

added theorem qExpansion_of_pow

added theorem qExpansion_one

added theorem qExpansion_smul

added theorem qExpansion_sub

added theorem qExpansion_zero