Theorem Derivative.normalizedDerivOfComplex_add

Modification history

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