norm_mul_cos_add_sin_mul_I — Mathlib

English

For any complex x, x equals its modulus times the vector (cos(arg x) + i sin(arg x)).

Русский

Для любого комплексного числа x выполняется полярное разложение: x = |x| (cos(arg x) + i sin(arg x)).

LaTeX

$$$x = \\|x\\| (\\\\cos(\\\\arg x) + i \\\\sin(\\\\arg x))$$$

Lean4

@[simp]
theorem norm_mul_cos_add_sin_mul_I (x : ℂ) : (‖x‖ * (cos (arg x) + sin (arg x) * I) : ℂ) = x := by
  rw [← exp_mul_I, norm_mul_exp_arg_mul_I]

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