angle_one_right

Mathlib.Analysis.Complex.Angle

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

English

For a nonzero x, the angle between x and 1 equals the absolute value of the argument of x.

Русский

Для ненулевого x, угол между x и 1 равен модулю аргумента x.

LaTeX

$$$$\angle(x,1) = |\arg(x)| \quad (x \ne 0).$$$$

Lean4

theorem angle_one_right (hx : x ≠ 0) : angle x 1 = |x.arg| := by simp [angle_eq_abs_arg, hx]

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

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

Разделы

Аффилиация

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