someRayVector_ray — Mathlib

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 _

Похожие утверждения