Theorem UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.qExpansion_coeff_zero

Modification history

2026-05-25 07:57
Mathlib/NumberTheory/ModularForms/QExpansion.lean
feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms (#38993) …
Added UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.qExpansion_coeff_zeroView on Github →