angle_neg_right — Mathlib

English

The angle between x and a negative multiple of y equals the angle between x and -y.

Русский

Угол между x и отрицательной кратностью y равен углу между x и -y.

LaTeX

$$$\\\\angle x (r \\\\cdot y) = \\\\angle x (-y)$, если $r<0$$$

Lean4

/-- The angle between a vector and the negation of another vector. -/
theorem angle_neg_right (x y : V) : angle x (-y) = π - angle x y :=
  by
  unfold angle
  rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]

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