arctan — Mathlib

English

The complex arctangent is defined by arctan(z) = -(i/2) log((1 + z i)/(1 - z i)).

Русский

Комплексное арктангенс определяется как arctan(z) = -(i/2) log((1 + i z)/(1 - i z)).

LaTeX

$$$\\operatorname{arctan}(z) = -\\frac{i}{2}\\, \\log\\left(\\frac{1 + z i}{1 - z i}\\right).$$$

Lean4

/-- The complex arctangent, defined via the complex logarithm. -/
noncomputable def arctan (z : ℂ) : ℂ :=
  -I / 2 * log ((1 + z * I) / (1 - z * I))

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