English
For nonzero vectors v1,v2, their rays are equal if and only if v1 and v2 lie on the same ray.
Русский
Для ненулевых векторов v1 и v2 лучи равны тогда и только тогда, когда они лежат на одном луче.
LaTeX
$$$ v_1 \neq 0, \ v_2 \neq 0 : \operatorname{rayOfNeZero}(R, v_1) = \operatorname{rayOfNeZero}(R, v_2) \iff \operatorname{SameRay}(R, v_1, v_2). $$$
Lean4
/-- Equivalence of nonzero vectors, in terms of `SameRay`. -/
theorem equiv_iff_sameRay {v₁ v₂ : RayVector R M} : v₁ ≈ v₂ ↔ SameRay R (v₁ : M) v₂ :=
Iff.rfl