mathlib3

765955fb - feat(linear_algebra/ray): `iff` versions of some lemmas (#16642)

feat(linear_algebra/ray): `iff` versions of some lemmas (#16642) Add `iff` versions of some `same_ray` lemmas. These are lemmas where we already have some form of both directions, but not the `iff` version (and the separate directions are still useful on their own, since one direction is true for weaker typeclass assumptions than the `iff` version and the other is available with dot notation).