English
The complex power function is defined by cpow(x,y) = exp(y log x) when x ≠ 0, with 0^0 = 1 and 0^y = 0 for y ≠ 0.
Русский
Комплексная степенная функция определяется как cpow(x,y) = exp(y log x) при x ≠ 0, при этом 0^0 = 1 и 0^y = 0 для y ≠ 0.
LaTeX
$$$$ \text{cpow}(x,y) = \begin{cases} 1, & x=0, y=0, \\ 0, & x=0, y\neq 0, \\ \exp(y \log x), & x\neq 0. \end{cases} $$$$
Lean4
/-- The complex power function `x ^ y`, given by `x ^ y = exp(y log x)` (where `log` is the
principal determination of the logarithm), unless `x = 0` where one sets `0 ^ 0 = 1` and
`0 ^ y = 0` for `y ≠ 0`. -/
noncomputable def cpow (x y : ℂ) : ℂ :=
if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
