oangle_sign_neg_right — Mathlib

English

Negating the second vector flips the sign of the oangle: (o.oangle x (−y)).sign = −(o.oangle x y).sign (duplicate illustration).

Русский

Отрицание второго вектора меняет знак oangle: (o.oangle x (−y)).sign = −(o.oangle x y).sign.

LaTeX

$$$ (o.oangle x (-y)).sign = -(o.oangle x y).sign $$$

Lean4

/-- Negating the second vector passed to `oangle` negates the sign of the angle. -/
@[simp]
theorem oangle_sign_neg_right (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign :=
  by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi]

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