cpow_ofReal_im — Mathlib

English

For a complex x and real y, the imaginary part of x^y equals |x|^y · sin(arg x · y).

Русский

Для комплексного числа x и вещественного y мнимая часть x^y равна |x|^y · sin(arg x · y).

LaTeX

$$$\operatorname{Im}(x^{y}) = |x|^{y} \sin(\arg x \cdot y)$$$

Lean4

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

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