English
The ray of a positive multiple of a nonzero vector equals the ray of the vector itself.
Русский
Луч положительного множителя ненулевого вектора совпадает с лучом самого вектора.
LaTeX
$$@[simp] $ \operatorname{rayOfNeZero}(R, r \cdot v) = \operatorname{rayOfNeZero}(R, v) $ for 0 < r and v ≠ 0.$$
Lean4
/-- The ray given by a positive multiple of a nonzero vector. -/
@[simp]
theorem ray_pos_smul {v : M} (h : v ≠ 0) {r : R} (hr : 0 < r) (hrv : r • v ≠ 0) :
rayOfNeZero R (r • v) hrv = rayOfNeZero R v h :=
(ray_eq_iff _ _).2 <| SameRay.sameRay_pos_smul_left v hr