angle_one_left

Mathlib.Analysis.Complex.Angle

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

English

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

Русский

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

LaTeX

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

Lean4

theorem angle_one_left (hy : y ≠ 0) : angle 1 y = |y.arg| := by simp [angle_eq_abs_arg, hy]

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

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

Разделы

Аффилиация

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