English
For nonzero x,y,z, the negated cyclic sum equals π, consistent with sum of triangle angles.
Русский
Для ненулевых x,y,z сумма с отрицаниями по циклу равна π; это аналог суммы углов треугольника.
LaTeX
$$o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = π$$
Lean4
/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the first
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_left {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
rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx,
show
o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) =
o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle)
by abel,
o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add]
