cot_pi_mul_contDiffWithinAt — Mathlib

English

See item 61148 for cotangent with exponential expression, now with π embedded.

Русский

См. пункт 61148 для котангенса через экспоненты с встроенным π.

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_mul_contDiffWithinAt (k : ℕ∞) (hx : x ∈ ℂ_ℤ) : ContDiffWithinAt ℂ k (fun x ↦ (↑π * x).cot) ℍₒ x :=
  by
  simp_rw [Complex.cot, Complex.cos, Complex.sin]
  exact ContDiffWithinAt.div (by fun_prop) (by fun_prop) (sin_pi_mul_ne_zero hx)

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