Theorem ModularForm.differentiableAt_eta_tprod

Modification history

2026-02-05 18:04

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

feat(NumberTheory/ModularForms/DedekindEta): Show logDeriv eta is E2 (#34217) …

Added ModularForm.differentiableAt_eta_tprod View on Github →