Theorem ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_eta

Modification history

2026-03-31 07:42
Mathlib/NumberTheory/ModularForms/Delta.lean
feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …
Modified ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_etaView on Github →
2026-03-06 23:58
Mathlib/NumberTheory/ModularForms/Delta.lean
feat(ModularForm/NumberTheory/Delta): Define the delta function (#34881) …
Added ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_etaView on Github →