Theorem ModularForm.csqrt_I_pow_24

Modification history

2026-03-31 07:42

Mathlib/NumberTheory/ModularForms/Delta.lean

feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …

Modified ModularForm.csqrt_I_pow_24 View on Github →

2026-03-06 23:58

Mathlib/NumberTheory/ModularForms/Delta.lean

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

Added ModularForm.csqrt_I_pow_24 View on Github →