Theorem ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow

Modification history

2026-05-01 08:23
Mathlib/NumberTheory/ModularForms/Discriminant.lean
feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979) …
Added ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_powView on Github →