Linear indep of nonzero smul

Stream: Is there code for X?

[Adam Topaz]

Do we have something like this?

import linear_algebra.linear_independent

variables (K V : Type*) [field K] [add_comm_group V] [vector_space K V]

lemma foo {ι : Type*} (f g : ι → V) (cond : ∀ i, ∃ a : K, a ≠ 0 ∧ a • f i = g i) :
  linear_independent K f ↔ linear_independent K g := sorry