arg_one

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

The argument of 1 is 0: arg(1) = 0.

Русский

Аргумент единицы равен 0: arg(1) = 0.

LaTeX

$$$\\\\arg 1 = 0$$$

Lean4

@[simp]
theorem arg_one : arg 1 = 0 := by simp [arg, zero_le_one]

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

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

Разделы

Аффилиация

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