Theorem ModularForm.logDeriv_eta_eq_E2

Modification history

2026-02-05 18:04

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

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

Added ModularForm.logDeriv_eta_eq_E2 View on Github →