arg_of_im_pos

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

← MathLib Explorer

English

If Im(z) > 0, then arg z = arccos(Re(z)/||z||).

Русский

Если Im(z) > 0, то arg z = arccos(Re(z)/||z||).

LaTeX

$$$$ \arg z = \arccos\left( \frac{\operatorname{Re}(z)}{\|z\|} \right), \quad 0 < \operatorname{Im}(z). $$$$

Lean4

theorem arg_of_im_pos {z : ℂ} (hz : 0 < z.im) : arg z = Real.arccos (z.re / ‖z‖) :=
  arg_of_im_nonneg_of_ne_zero hz.le fun h => hz.ne' <| h.symm ▸ rfl

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

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

Разделы

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

Аффилиация

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