arg_neg_eq_arg_sub_pi_of_im_pos

Mathlib.Analysis.SpecialFunctions.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.arg_neg_eq_arg_sub_pi_of_im_pos

← MathLib Explorer

English

If Im x > 0 then arg(-x) = arg x - π.

Русский

Если Im x > 0, то arg(-x) = arg x - π.

LaTeX

$$$\\\\text{If } x \\\\text{ has } \\\\Im x > 0, \\\\text{ then } \\\\arg(-x) = \\\\arg x - \\\\pi$$$

Lean4

theorem arg_neg_eq_arg_sub_pi_of_im_pos {x : ℂ} (hi : 0 < x.im) : arg (-x) = arg x - π :=
  by
  rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]
  simp [neg_div, Real.arccos_neg]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru