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.
Canonical embedding of the upper half-plane into ℂ
.
Instances For
Extensionality lemma in terms of UpperHalfPlane.re
and UpperHalfPlane.im
.
Constructor for UpperHalfPlane
. It is useful if ⟨z, h⟩
makes Lean use a wrong
typeclass instance.
Instances For
Numerator of the formula for a fractional linear transformation
Instances For
Denominator of the formula for a fractional linear transformation
Instances For
Fractional linear transformation, also known as the Moebius transformation
Instances For
Fractional linear transformation, also known as the Moebius transformation
Instances For
The action of GLPos 2 ℝ
on the upper half-plane by fractional linear transformations.