norm_mul_exp_arg_mul_I — Mathlib

English

Every complex number x can be written in polar form as x = |x| e^{i arg x}.

Русский

Каждое комплексное число x записывается в полярной форме как x = |x| e^{i arg x}.

LaTeX

$$$x = \\|x\\| \\\\mathrm{e}^{i\\\\arg x}$$$

Lean4

@[simp]
theorem norm_mul_exp_arg_mul_I (x : ℂ) : ‖x‖ * exp (arg x * I) = x :=
  by
  rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  · have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx
    apply Complex.ext <;> simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

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