Manifold

Statistics

Metric	Count
Definitions	0
Theorems `mdifferentiable_jacobiTheta`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiable_jacobiTheta` 📖	mathematical	—	`MDifferentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.instChartedSpaceComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `chartedSpaceSelf` `jacobiTheta` `UpperHalfPlane.coe`	—	`MDifferentiableAt.comp` `DifferentiableAt.mdifferentiableAt` `differentiableAt_jacobiTheta` `UpperHalfPlane.coe_im_pos` `UpperHalfPlane.mdifferentiable_coe`

---