English
Let x ∈ ℂ. The principal logarithm log x is defined by log x = log|x| + i Arg(x), where Arg(x) ∈ (-π, π], and log 0 = 0. In particular, -π < Im(log x) ≤ π, and log is the inverse of exp on nonzero complex numbers when restricted to this branch.
Русский
Пусть x ∈ ℂ. Главный комплексный логарифм log x задаётся формулой log x = log|x| + i Arg(x), где Arg(x) ∈ (-π, π], и log 0 = 0. В частности, -π < Im(log x) ≤ π, и экспонента является обратной к log на ненулевых комплексных числах при ограничении на эту ветку.
LaTeX
$$$\log x = \operatorname{Real}\log \|x\| + \operatorname{Arg}(x)\, i, \quad \log 0 = 0, \quad -\pi < \operatorname{Im}(\log x) \le \pi.$$$
Lean4
/-- Inverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
`log 0 = 0` -/
@[pp_nodot]
noncomputable def log (x : ℂ) : ℂ :=
Real.log ‖x‖ + arg x * I
