oangle_sign_smul_left — Mathlib

English

Multiplying the first vector by r scales the sign of the oangle by the sign of r (a standard sign rule).

Русский

Умножение первого вектора на r масштабирует знак ориентированного угла на знак r.

LaTeX

$$$ (o.oangle (r \cdot x) y).sign = \operatorname{sign}(r) \cdot (o.oangle x y).sign $$$

Lean4

/-- Multiplying the first vector passed to `oangle` by a real multiplies the sign of the angle by
the sign of the real. -/
@[simp]
theorem oangle_sign_smul_left (x y : V) (r : ℝ) : (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign :=
  by rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h]

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