English
From a ray x, taking the representative someRayVector and forming its ray yields the original ray: ray(x.someRayVector) = x.
Русский
Из луча x, взяв представителя someRayVector и построив его луч, получаем исходный луч: ray(x.someRayVector) = x.
LaTeX
$$$\text{someRayVectorRay}(x)\;:\; \text{rayOfNeZero}(R, x.someVector\_ne\_zero) = x.$$$
Lean4
/-- The ray of `someRayVector`. -/
@[simp]
theorem someRayVector_ray (x : Module.Ray R M) : (⟦x.someRayVector⟧ : Module.Ray R M) = x :=
Quotient.out_eq _