Theorem Derivative.normalizedDerivOfComplex_mdifferentiable

Modification history

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