not independent of mem span

Stream: Is there code for X?

[Scott Morrison]

Do we have

import linear_algebra.linear_independent

open submodule

variables {ι : Type*}
variables {R : Type*} [ring R]
variables {M : Type*} [add_comm_group M] [module R M]

example (w : set ι) (x : ι) (n : x ∉ w) (v : ι → M) (h : v x ∈ span R (v '' w)) :
  ¬ linear_independent R v :=
sorry

somewhere?

[Scott Morrison]

lemma linear_independent.not_mem_span_image [nontrivial R] (hv : linear_independent R v) {s : set ι}
  {x : ι} (h : x ∉ s) :
  v x ∉ submodule.span R (v '' s) :=
begin
  have h' : v x ∈ submodule.span R (v '' {x}),
  { rw set.image_singleton,
    exact mem_span_singleton_self (v x), },
  intro w,
  apply linear_independent.ne_zero x hv,
  refine disjoint_def.1 (hv.disjoint_span_image _) (v x) h' w,
  simpa using h,
end

does it.