arg_eq_pi_iff_lt_zero

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

Arg z = π iff z.re < 0 and z.im = 0 (same content as Pi criterion).

Русский

Arg z = π эквивалентно z.re < 0 и z.im = 0 (тот же критерий).

LaTeX

$$$$ \arg z = \pi \iff (z.re < 0) \land (z.im = 0). $$$$

Lean4

theorem arg_eq_pi_iff_lt_zero {z : ℂ} : arg z = π ↔ z < 0 :=
  arg_eq_pi_iff

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

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

Разделы

Аффилиация

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