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 UpperHalfPlane.abs_exp_two_pi_I_lt_one (z : UpperHalfPlane) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑z)‖ < 1