oangle_sign_sub_right_swap — Mathlib

English

The sign of the angle between two linear combinations of x and y depends on the determinant of the coefficient matrix and the sign of the angle between x and y.

Русский

Знак угла между двумя линейными комбинациями x и y зависит от детерминанта матрицы коэффициентов и знака угла между x и y.

LaTeX

$$$\\operatorname{sign}(o.oangle( r_1 x + r_2 y, r_3 x + r_4 y )) = \\operatorname{sign}(r_1 r_4 - r_2 r_3) \\cdot \\operatorname{sign}( o.oangle(x,y) )$$$

Lean4

/-- Subtracting the first vector passed to `oangle` from the second vector then swapping the
vectors does not change the sign of the angle. -/
@[simp]
theorem oangle_sign_sub_right_swap (x y : V) : (o.oangle y (y - x)).sign = (o.oangle x y).sign := by
  rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

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