ExpLems

theorem exp_upperHalfPlane_lt_one (z : UpperHalfPlane) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑z)‖ < 1

theorem exp_upperHalfPlane_lt_one_nat (z : UpperHalfPlane) (n : ℕ) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)‖ < 1

theorem exp_periodo (z : UpperHalfPlane) (n : ℕ) : Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * (1 + ↑z)) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑z)