linear_independent lemmas

Stream: Is there code for X?

[Scott Morrison]

I've realised I can work around needing this, so I don't think I'm going to prove this for my current project, but I'm curious if we have something that quickly proves:

import linear_algebra.linear_independent

open_locale classical

variables {ι : Type*} {R M : Type*} [ring R] [add_comm_group M] [module R M] (v : ι → M)

lemma linear_independent.total_ne_total_of_support_sdiff_support (hv : linear_independent R v)
  (f g : ι →₀ R) (x ∈ f.support \ g.support) :
  finsupp.total ι M R v f ≠ finsupp.total ι M R v g :=
sorry

[Scott Morrison]

I guess one just shows x ∈ (f - g).support, and linearity of finsupp.total.

[Johan Commelin]

finsupp.total is linear by definition, right?

[Scott Morrison]

Yes

[Heather Macbeth]

lemma linear_independent.total_ne_total_of_support_sdiff_support (hv : linear_independent R v)
  (f g : ι →₀ R) (x ∈ f.support \ g.support) :
  finsupp.total ι M R v f ≠ finsupp.total ι M R v g :=
begin
  contrapose! H,
  simp [hv.total_equiv.injective (subtype.ext H)]
end

[Scott Morrison]

kawow! :-)

[Johan Commelin]

Quite surprising that the proof doesn't mention x