oangle_sub_left — Mathlib

English

For nonzero x,y,z, the cyclic sum o.oangle x y + o.oangle y z + o.oangle z x equals 0.

Русский

Для ненулевых x,y,z сумма по циклу o.oangle x y + o.oangle y z + o.oangle z x равна 0.

LaTeX

$$o.oangle x y + o.oangle y z + o.oangle z x = 0$$

Lean4

/-- Given three nonzero vectors, the angle between the first and the third minus the angle
between the first and the second equals the angle between the second and the third. -/
@[simp]
theorem oangle_sub_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x z - o.oangle x y = o.oangle y z := by rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]

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