cot_pi_eq_exp_ratio — Mathlib

English

Cotangent scaled by pi also has a standard exponential expression: cot(π z) = (e^{2π i z} + 1)/(i(1 - e^{2π i z})).

Русский

Котангенс с множителем π имеет экспоненциальное выражение: cot(π z) = (e^{2π i z} + 1)/(i(1 - e^{2π i z})).

LaTeX

$$$$\forall z \in \mathbb{C}, \; \cot(\pi z) = \frac{e^{2\pi i z} + 1}{i\bigl(1 - e^{2\pi i z}\bigr)}.$$$$

Lean4

theorem cot_pi_eq_exp_ratio (z : ℂ) :
    cot (π * z) = (Complex.exp (2 * π * I * z) + 1) / (I * (1 - Complex.exp (2 * π * I * z))) :=
  by
  rw [cot_eq_exp_ratio (π * z)]
  ring_nf
    /- This is the version one probably wants, which is why the pi's are there. -/

Похожие утверждения