Theorem Function.Periodic.differentiable_qParam

Modification history

2025-08-25 12:07
Mathlib/Analysis/Complex/Periodic.lean
feat(NumberTheory/ModularForms): the Dedekind Eta function (#28400) …
Added Function.Periodic.differentiable_qParamView on Github →