arg_neg_eq_arg_add_pi_of_im_neg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\\\\Im x < 0 \\\\Rightarrow \\\\arg(-x) = \\\\arg x + \\\\pi$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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