two vectors have the same direction

Stream: maths

[Yury G. Kudryashov]

There are quite a few ways to say that two vectors in a real vector space have the same direction (or at least one of them is zero). Do we have some iff/tfae lemmas about this?
@Heather Macbeth @Frédéric Dupuis , you probably needed something like that in rayleigh*

[Eric Wieser]

docs#same_ray is perhaps one such spelling

[Heather Macbeth]

It was all quite cumbersome -- I think we tried to restrict to the sphere as soon as possible.

[Yury G. Kudryashov]

@Eric Wieser I want a similar relation, namely "same_ray or one of the vectors is zero". How should I call it?

[Yury G. Kudryashov]

BTW, over the field it is equivalent to orbit_rel for the induced action of positive elements, not for the action of the original field.

[Eric Wieser]

Yury G. Kudryashov said:

BTW, over the field it is equivalent to orbit_rel for the induced action of positive elements, not for the action of the original field.

To be clear, you're saying the current docstring is wrong, right? Indeed, docs#same_ray_setoid_eq_orbit_rel has the correct statement

[Eric Wieser]

Something like this?

import algebra.order.ring
import algebra.module
import linear_algebra.orientation

variables (R : Type*) [ordered_comm_semiring R] {M : Type*} [add_comm_monoid M] [module R M]

def same_ray₀ (v₁ v₂ : M) : Prop :=
∃ (r₁ r₂ : R), 0 < (r₁, r₂) ∧ r₁ • v₁ = r₂ • v₂

variables {R}

lemma same_ray.same_ray₀ {v₁ v₂ : M} : same_ray R v₁ v₂ → same_ray₀ R v₁ v₂ :=
Exists₂.imp $ λ r₁ r₂ ⟨hr₁, hr₂, h⟩, ⟨prod.mk_lt_mk.mpr $ or.inl ⟨hr₁, hr₂.le⟩, h⟩

[Eric Wieser]

Maybe we should just redefine same_ray to mean that though?

[Eric Wieser]

I think all the uses of same_ray are on docs#ray_vector anyway which is never zero, so the difference doesn't matter