arg_eq_zero_iff_zero_le

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

Arg z = 0 iff z lies on the nonnegative real axis (0 ≤ z).

Русский

Arg z = 0 если и только если z лежит на неотрицательной вещественной оси (0 ≤ z).

LaTeX

$$$$ \arg z = 0 \iff z \text{ lies on the nonnegative real axis}. $$$$

Lean4

theorem arg_eq_zero_iff_zero_le {z : ℂ} : arg z = 0 ↔ 0 ≤ z := by rw [arg_eq_zero_iff, eq_comm, nonneg_iff]

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

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

Разделы

Аффилиация

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