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).

src/linear_algebra/ray.lean

@@ -577,3 +577,48 @@ lemma exists_eq_smul (h : same_ray R v₁ v₂) :
 ⟨v₁ + v₂, h.exists_eq_smul_add⟩
 
 end same_ray
+
+section linear_ordered_field
+
+variables {R : Type*} [linear_ordered_field R]
+variables {M : Type*} [add_comm_group M] [module R M] {x y : M}
+
+lemma exists_pos_left_iff_same_ray (hx : x ≠ 0) (hy : y ≠ 0) :
+  (∃ r : R, 0 < r ∧ r • x = y) ↔ same_ray R x y :=
+begin
+  refine ⟨λ h, _, λ h, h.exists_pos_left hx hy⟩,
+  rcases h with ⟨r, hr, rfl⟩,
+  exact same_ray_pos_smul_right x hr
+end
+
+lemma exists_pos_left_iff_same_ray_and_ne_zero (hx : x ≠ 0) :
+  (∃ r : R, 0 < r ∧ r • x = y) ↔ (same_ray R x y ∧ y ≠ 0) :=
+begin
+  split,
+  { rintro ⟨r, hr, rfl⟩,
+    simp [hx, hr.le, hr.ne'] },
+  { rintro ⟨hxy, hy⟩,
+    exact (exists_pos_left_iff_same_ray hx hy).2 hxy }
+end
+
+lemma exists_nonneg_left_iff_same_ray (hx : x ≠ 0) :
+  (∃ r : R, 0 ≤ r ∧ r • x = y) ↔ same_ray R x y :=
+begin
+  refine ⟨λ h, _, λ h, h.exists_nonneg_left hx⟩,
+  rcases h with ⟨r, hr, rfl⟩,
+  exact same_ray_nonneg_smul_right x hr
+end
+
+lemma exists_pos_right_iff_same_ray (hx : x ≠ 0) (hy : y ≠ 0) :
+  (∃ r : R, 0 < r ∧ x = r • y) ↔ same_ray R x y :=
+by simpa only [same_ray_comm, eq_comm] using exists_pos_left_iff_same_ray hy hx
+
+lemma exists_pos_right_iff_same_ray_and_ne_zero (hy : y ≠ 0) :
+  (∃ r : R, 0 < r ∧ x = r • y) ↔ (same_ray R x y ∧ x ≠ 0) :=
+by simpa only [same_ray_comm, eq_comm] using exists_pos_left_iff_same_ray_and_ne_zero hy
+
+lemma exists_nonneg_right_iff_same_ray (hy : y ≠ 0) :
+  (∃ r : R, 0 ≤ r ∧ x = r • y) ↔ same_ray R x y :=
+by simpa only [same_ray_comm, eq_comm] using exists_nonneg_left_iff_same_ray hy
+
+end linear_ordered_field