Theorem mdifferentiable_jacobiTheta

Modification history

2026-03-02 23:05

Mathlib/NumberTheory/ModularForms/JacobiTheta/Manifold.lean

chore(NumberTheory/ModularForms): golf using custom elaborators (#35730) …

Modified mdifferentiable_jacobiTheta View on Github →

2023-07-02 18:13

Mathlib/NumberTheory/ModularForms/JacobiTheta/Manifold.lean

feat: port NumberTheory.ModularForms.JacobiTheta.Manifold (#5670)

Added mdifferentiable_jacobiTheta View on Github →