Exp on the upper half plane #
This file contains lemmas about the exponential function on the upper half plane. Useful for q-expansions of modular forms.
theorem
Function.Periodic.im_invQParam_pos_of_abs_lt_one
{h : ℝ}
(hh : 0 < h)
{q : ℂ}
(hq : Complex.abs q < 1)
(hq_ne : q ≠ 0)
: