Linear combination description of span

Stream: Is there code for X?

[Adam Topaz]

Hi everyone. I was again having trouble finding some simple facts in mathlib, this time from linear algebra. Does mathlib contain a complete description of the span as the collection of linear combinations?

I am aware of finsupp.mem_span_iff_total but I found this cumbersome to work with (this is probably entirely due to the fact that I don't have much experience with mathlib).

Anyway, I wrote up this alternative description, in case there isn't something similar in mathlib and it might be helpful for someone.
https://github.com/adamtopaz/mathlib/blob/lcspan/src/linear_algebra/lincomb.lean

[Mario Carneiro]

The collection of linear combinations used to be called lc but I think now it's just finsupp

[Mario Carneiro]

yeah it's finsupp.mem_span_iff_total