oangle_neg_orientation_eq_neg — Mathlib

English

Negating the orientation negates the value of the oriented angle: (−o).oangle x y = − o.oangle x y.

Русский

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

LaTeX

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

Lean4

/-- Negating the orientation negates the value of `oangle`. -/
theorem oangle_neg_orientation_eq_neg (x y : V) : (-o).oangle x y = -o.oangle x y := by simp [oangle]

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