Theorem ModularForm.logDeriv_one_sub_mul_cexp_comp

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_mul_cexp_compView on Github →