oangle_add_cyc3_neg_right — Mathlib

English

If ‖x‖ = ‖y‖, then o.oangle x (x - y) = o.oangle (y - x) y.

Русский

Если ‖x‖ = ‖y‖, то o.oangle x (x - y) = o.oangle (y - x) y.

LaTeX

$$$o.oangle x (x - y) = o.oangle (y - x) y \text{ при } \|x\| = \|y\|$$$

Lean4

/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the second
vector in each angle negated, results in π. If the vectors add to 0, this is a version of the
sum of the angles of a triangle. -/
@[simp]
theorem oangle_add_cyc3_neg_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = π := by
  simp_rw [← oangle_neg_left_eq_neg_right, o.oangle_add_cyc3_neg_left hx hy hz]

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