Manifold structure on the upper half plane. #
In this file we define the complex manifold structure on the upper half-plane.
The inclusion map ℍ → ℂ
is a smooth map of manifolds.
The inclusion map ℍ → ℂ
is a differentiable map of manifolds.
Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
In this file we define the complex manifold structure on the upper half-plane.
The inclusion map ℍ → ℂ
is a smooth map of manifolds.
The inclusion map ℍ → ℂ
is a differentiable map of manifolds.