English
The oriented angle between x and y is zero exactly when x and y lie on the same ray.
Русский
Ориентированный угол между x и y равен нулю тогда и только тогда, когда x и y лежат на одной луче.
LaTeX
$$$o.oangle x y = 0 \iff \text{SameRay}_{\mathbb{R}}(x,y)$$$
Lean4
/-- The oriented angle between two vectors is zero if and only if they are on the same ray. -/
theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y :=
by
rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
Complex.arg_eq_zero_iff]
simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y