English
The cotangent can be expressed in terms of exponentials as cot z = (e^{2iz} + 1) / (i(1 - e^{2iz})).
Русский
Котангенс выражается через экспоненты: cot z = (e^{2iz} + 1) / (i(1 - e^{2iz})).
LaTeX
$$$$\forall z \in \mathbb{C}, \; \cot z = \frac{e^{2 i z} + 1}{i\bigl(1 - e^{2 i z}\bigr)}.$$$$
Lean4
theorem cot_eq_exp_ratio (z : ℂ) : cot z = (Complex.exp (2 * I * z) + 1) / (I * (1 - Complex.exp (2 * I * z))) :=
by
rw [Complex.cot, Complex.sin, Complex.cos]
have h1 : exp (z * I) + exp (-z * I) = exp (-(z * I)) * (exp (2 * I * z) + 1) :=
by
rw [mul_add, ← Complex.exp_add]
simp only [mul_one]
ring_nf
have h2 : (exp (-z * I) - exp (z * I)) = exp (-(z * I)) * ((1 - exp (2 * I * z))) :=
by
ring_nf
rw [mul_assoc, ← Complex.exp_add]
ring_nf
rw [h1, h2]
field_simp
/- The version one probably wants to use more. -/
