feat(linear_algebra/ray): relation to linear independence (#16056)
feat(linear_algebra/ray): relation to linear independence (#16056)

Add lemmas that two vectors are linearly dependent if and only if
they are in the same ray or one is in the same ray as the negation of
the other (for a module over a `linear_ordered_comm_ring` with
`no_zero_smul_divisors`).







leanprover-community/mathlib,leanprover-community/mathlib