arg_ofReal_of_neg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

If x is a negative real number, then arg x = π.

Русский

Если x — отрицательное действительное число, то arg x = π.

LaTeX

$$$$ \arg x = \pi \quad \text{for } x \in \mathbb{R},\ x<0. $$$$

Lean4

theorem arg_ofReal_of_neg {x : ℝ} (hx : x < 0) : arg x = π :=
  arg_eq_pi_iff.2 ⟨hx, rfl⟩

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

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

Разделы

Аффилиация

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