English
If two vectors lie on the same ray, then multiplying both by the same action preserves being on the same ray.
Русский
Если два вектора лежат на одном луче, одновременное умножение на одно и то же действие сохраняет их принадлежность одному лучу.
LaTeX
$$$ \operatorname{SameRay}(R, x, y) \Rightarrow \operatorname{SameRay}(R, s\cdot x, s\cdot y), \; \forall s \in S.$$$
Lean4
/-- If two vectors are on the same ray then both scaled by the same action are also on the same
ray. -/
theorem smul {S : Type*} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (h : SameRay R x y) (s : S) :
SameRay R (s • x) (s • y) :=
h.map (s • (LinearMap.id : M →ₗ[R] M))
