Cotangent

This file contains lemmas about the cotangent function, including useful series expansions.

theorem Complex.cot_eq_exp_ratio (z : ℂ) : z.cot = (Complex.exp (2 * Complex.I * z) + 1) / (Complex.I * (1 - Complex.exp (2 * Complex.I * z)))

theorem Complex.cot_pi_eq_exp_ratio (z : ℂ) : (↑Real.pi * z).cot = (Complex.exp (2 * ↑Real.pi * Complex.I * z) + 1) / (Complex.I * (1 - Complex.exp (2 * ↑Real.pi * Complex.I * z)))

theorem pi_mul_cot_pi_q_exp (z : UpperHalfPlane) : ↑Real.pi * (↑Real.pi * ↑z).cot = ↑Real.pi * Complex.I - 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n