oangle_smul_right_of_neg — Mathlib

English

Multiplying the first vector by a positive real does not change the angle: o.oangle (r·x) y = o.oangle x y, if r > 0.

Русский

Умножение первого вектора на положительное число не изменяет угол: o.oangle (r·x) y = o.oangle x y при r > 0.

LaTeX

$$$r>0 \Rightarrow o.oangle\;(r\cdot x)\;y = o.oangle\;x\;y$$$

Lean4

/-- Multiplying the second vector passed to `oangle` by a negative real produces the same angle
as negating that vector. -/
@[simp]
theorem oangle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) : o.oangle x (r • y) = o.oangle x (-y) := by
  rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)]

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