sin_arg — Mathlib

English

For any complex number x, the sine of its argument equals the imaginary part divided by its modulus: sin(arg x) = Im(x)/|x|.

Русский

Для любого комплексного числа x синус аргумента x равен мнимой части x, делённой на модуль x: sin(arg x) = Im(x)/|x|.

LaTeX

$$$\\\\sin(\\\\arg z) = \\\\frac{\\\\Im(z)}{\\\\|z\\\\|}$$$

Lean4

theorem sin_arg (x : ℂ) : Real.sin (arg x) = x.im / ‖x‖ := by unfold arg;
  split_ifs <;>
    simp [sub_eq_add_neg,
      Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1 (abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add,
      neg_div, Real.arcsin_neg, Real.sin_neg]

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