Theorem ModularFormClass.qExpansionFormalMultilinearSeries_coeff

Modification history

2026-02-16 13:52
Mathlib/NumberTheory/ModularForms/QExpansion.lean
feat(NumberTheory/ModularForms/QExpansion): define qExpansion ring hom and some more API (#32959) …
Added ModularFormClass.qExpansionFormalMultilinearSeries_coeffView on Github →