Theorem ModularForm.eta_ne_zero

Modification history

2026-02-05 18:04
Mathlib/NumberTheory/ModularForms/DedekindEta.lean
feat(NumberTheory/ModularForms/DedekindEta): Show logDeriv eta is E2 (#34217) …
Modified ModularForm.eta_ne_zeroView on Github →
2025-08-25 12:07
Mathlib/NumberTheory/ModularForms/DedekindEta.lean
feat(NumberTheory/ModularForms): the Dedekind Eta function (#28400) …
Added ModularForm.eta_ne_zeroView on Github →