Theorem ModularFormClass.continuous

Modification history

2025-12-04 09:22
Mathlib/NumberTheory/ModularForms/Basic.lean
feat(NumberTheory/ModularForms): improvements to q-expansions (#32060) …
Modified ModularFormClass.continuousView on Github →
2025-09-23 06:31
Mathlib/NumberTheory/ModularForms/Basic.lean
feat(NumberTheory/ModularForms): integrand for Petersson product (#29640) …
Added ModularFormClass.continuousView on Github →