Def Derivative.normalizedDerivOfComplex

Modification history

2026-03-18 13:09
Mathlib/NumberTheory/ModularForms/Derivative.lean
feat(ModularForms): (normalized) derivative of modular forms (#36405) …
Added Derivative.normalizedDerivOfComplexView on Github →