mathlib3

9d24857b - 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`).