English
If a vector lies in the orbit of another under the Units.posSubgroup action, then the two vectors lie in the same ray.
Русский
Если вектор лежит в орбите другого в рамках действия Units.posSubgroup, значит два вектора лежат в одном луче.
LaTeX
$$$v_1 \in \mathrm{MulAction}.orbit(Units.posSubgroup R)\, v_2 \Rightarrow \mathrm{SameRay}(R, v_1, v_2).$$$
Lean4
/-- `SameRay` follows from membership of `MulAction.orbit` for the `Units.posSubgroup`. -/
theorem sameRay_of_mem_orbit {v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit (Units.posSubgroup R) v₂) : SameRay R v₁ v₂ :=
by
rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
exact SameRay.sameRay_pos_smul_left _ hr
