Theorem ModularForm.eta_tprod_ne_zero

Modification history

2026-02-05 18:04

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

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

Added ModularForm.eta_tprod_ne_zero View on Github →