cpow_def — Mathlib

English

The complex power is defined by cpow(x,y) = if x = 0 then if y = 0 then 1 else 0 else exp(log x · y).

Русский

Комплексная степень определяется как cpow(x,y) = если x = 0, то если y = 0 тогда 1, иначе 0; в противном случае exp(log x · y).

LaTeX

$$$$ x^{y} = \begin{cases} \exp( y \log x ), & x \neq 0, \\ 1, & x=0, y=0, \\ 0, & x=0, y \neq 0. \end{cases} $$$$

Lean4

theorem cpow_def (x y : ℂ) : x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) :=
  rfl

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