Theorem ModularForm.logDeriv_one_sub_cexp

Modification history

2025-08-25 12:07

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

feat(NumberTheory/ModularForms): the Dedekind Eta function (#28400) …

Added ModularForm.logDeriv_one_sub_cexp View on Github →