Theorem ModularForm.summable_logDeriv_one_sub_eta_q

Modification history

2026-02-05 18:04
Mathlib/NumberTheory/ModularForms/DedekindEta.lean
feat(NumberTheory/ModularForms/DedekindEta): Show logDeriv eta is E2 (#34217) …
Added ModularForm.summable_logDeriv_one_sub_eta_qView on Github →