Theorem UpperHalfPlane.comp_ofComplex

Modification history

2024-08-26 10:46
Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
feat: add lemmas for ofComplex evaluations outside UpperHalfPlane (#16005) …
Modified UpperHalfPlane.comp_ofComplexView on Github →
2024-05-27 14:30
Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
Eisenstein series are mdifferentiable (#11013) …
Added UpperHalfPlane.comp_ofComplexView on Github →