cpow_ofReal_re — Mathlib

English

If x ≤ 0 is real and y is complex, then (x : ℂ)^y = (-x : ℂ)^y · exp(π i y).

Русский

Если x ≤ 0 — действительное число и y комплексное, то (x)^y = (-x)^y · exp(π i y).

LaTeX

$$$x \le 0 \Rightarrow (x : \mathbb{C})^{y} = (-x : \mathbb{C})^{y} \cdot e^{\pi i y}$$$

Lean4

theorem cpow_ofReal_re (x : ℂ) (y : ℝ) : (x ^ (y : ℂ)).re = ‖x‖ ^ y * Real.cos (arg x * y) := by rw [cpow_ofReal];
  generalize arg x * y = z; simp [Real.cos]

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