Assumptions:
TeX:
\operatorname{atan}(z) = \frac{i}{2} \log\!\left(\frac{1 - i z}{1 + i z}\right) z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; -z i \notin \left[1, \infty\right)
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Atan | Inverse tangent | |
ConstI | Imaginary unit | |
Log | Natural logarithm | |
CC | Complex numbers | |
ClosedOpenInterval | Closed-open interval | |
Infinity | Positive infinity |
Source code for this entry:
Entry(ID("500c0a"), Formula(Equal(Atan(z), Mul(Div(ConstI, 2), Log(Div(Sub(1, Mul(ConstI, z)), Add(1, Mul(ConstI, z))))))), Variables(z), Assumptions(And(Element(z, CC), NotElement(Mul(Neg(z), ConstI), ClosedOpenInterval(1, Infinity)))))