Theorem ModularForm.eta_comp_eqOn_const_mul_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.eta_comp_eqOn_const_mul_csqrt_eta View on Github →

2026-03-06 23:58

Mathlib/NumberTheory/ModularForms/Delta.lean

feat(ModularForm/NumberTheory/Delta): Define the delta function (#34881) …

Added ModularForm.eta_comp_eqOn_const_mul_csqrt_eta View on Github →