English
For a complex number x and real y, x^y equals |x|^y times (cos(arg x · y) + i sin(arg x · y)).
Русский
Для комплексного числа x и действительного y выполняется x^y = |x|^y (cos(arg x · y) + i sin(arg x · y)).
LaTeX
$$$x \in \mathbb{C},\ y \in \mathbb{R}:\ x^{y} = |x|^{y}\,\big(\cos(\arg x\cdot y) + i\sin(\arg x \cdot y)\big)$$$
Lean4
theorem ofReal_cpow_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℂ) : (x : ℂ) ^ y = (-x : ℂ) ^ y * exp (π * I * y) :=
by
rcases hx.eq_or_lt with (rfl | hlt)
· rcases eq_or_ne y 0 with (rfl | hy) <;> simp [*]
have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne
rw [cpow_def_of_ne_zero hne, cpow_def_of_ne_zero (neg_ne_zero.2 hne), ← exp_add, ← add_mul, log, log, norm_neg,
arg_ofReal_of_neg hlt, ← ofReal_neg, arg_ofReal_of_nonneg (neg_nonneg.2 hx), ofReal_zero, zero_mul, add_zero]
