angle_div_right_eq_angle_mul_left

Mathlib.Analysis.Complex.Angle

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

← MathLib Explorer

English

For any nonzero a, the angle between x and y/a equals the angle between x a and y.

Русский

Для любого ненулевого a угол между x и y/a равен углу между x a и y.

LaTeX

$$$$\angle\left(x, \frac{y}{a}\right) = \angle\left(x a, y\right).$$$$

Lean4

theorem angle_div_right_eq_angle_mul_left (a x y : ℂ) : angle x (y / a) = angle (x * a) y := by
  rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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