mathlib

877f2e7a - refactor(linear_algebra/ray): redefine `same_ray` to allow zero vectors (#12618)

refactor(linear_algebra/ray): redefine `same_ray` to allow zero vectors (#12618) In a strictly convex space, the new definition is equivalent to the fact that the triangle inequality becomes an equality. The old definition was only used for nonzero vectors in `mathlib`. Also make the definition of `ray_vector` semireducible so that `ray_vector.setoid` can be an instance.