angle_neg_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The angle between the negation of a vector and another vector. -/
theorem angle_neg_left (x y : V) : angle (-x) y = π - angle x y := by rw [← angle_neg_neg, neg_neg, angle_neg_right]

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