arg_ofReal_of_nonneg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

If x is a nonnegative real number, then its argument is 0.

Русский

Если x — неотрицательное действительное число, то его аргумент равен 0.

LaTeX

$$$$ \arg(x) = 0 \quad \text{for all } x \in \mathbb{R}, \; x \ge 0. $$$$

Lean4

theorem arg_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) : arg x = 0 := by simp [arg, hx]

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

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

Разделы

Аффилиация

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