angle_mul_right

Mathlib.Analysis.Complex.Angle

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

English

If a ≠ 0, then the angle between x a and y a equals the angle between x and y, for any x,y.

Русский

Если a ≠ 0, то угол между x a и y a равен углу между x и y.

LaTeX

$$$$\angle(x a, y a) = \angle(x,y) \quad (a \ne 0).$$$$

Lean4

@[simp]
theorem angle_mul_right (ha : a ≠ 0) (x y : ℂ) : angle (x * a) (y * a) = angle x y := by
  simp [mul_comm, angle_mul_left ha]

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

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

Разделы

Аффилиация

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