arg_neg_one

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

The argument of −1 is π.

Русский

Аргумент −1 равен π.

LaTeX

$$$$ \arg(-1) = \pi. $$$$

Lean4

@[simp]
theorem arg_neg_one : arg (-1) = π := by simp [arg, le_refl, not_le.2 (zero_lt_one' ℝ)]

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

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

Разделы

Аффилиация

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