Theorem Derivative.serreDerivative_add

Modification history

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