The upper half plane and its automorphisms #
This file defines
UpperHalfPlane to be the upper half plane in
We furthermore equip it with the structure of a
GLPos 2 ℝ action by
fractional linear transformations.
We define the notation
ℍ for the upper half plane available in the locale
UpperHalfPlane so as not to conflict with the quaternions.
The action of
GLPos 2 ℝ on the upper half-plane by fractional linear transformations.