English
Two nonzero vectors are linearly independent iff the oriented angle is not 0 and not π.
Русский
Два ненулевых вектора линейно независимы тогда и только тогда, когда ориентированный угол не равен 0 и не равен π.
LaTeX
$$$o.oangle x y \neq 0 \land o.oangle x y \neq \pi \iff \text{LinearIndependent}_{\mathbb{R}}(x,y)$$$
Lean4
/-- Given three nonzero vectors, the angle between the first and the second plus the angle
between the second and the third equals the angle between the first and the third. -/
@[simp]
theorem oangle_add {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : o.oangle x y + o.oangle y z = o.oangle x z :=
by
simp_rw [oangle]
rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]
· congr 1
exact mod_cast Complex.arg_real_mul _ (by positivity : 0 < ‖y‖ ^ 2)
· exact o.kahler_ne_zero hx hy
· exact o.kahler_ne_zero hy hz
