angle_smul_right_of_neg — Mathlib

English

If r < 0, then the angle between x and r y equals the angle between x and -y.

Русский

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

LaTeX

$$$\\\\angle x (r \\cdot y) = \\\\angle x (-y)$ при $r<0$$$

Lean4

/-- The angle between a vector and a negative multiple of a vector. -/
@[simp]
theorem angle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) : angle x (r • y) = angle x (-y) := by
  rw [← neg_neg r, neg_smul, angle_neg_right, angle_smul_right_of_pos x y (neg_pos_of_neg hr), angle_neg_right]

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