# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Linear combination description of span

#### Adam Topaz (Jun 10 2020 at 21:53):

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 (Jun 10 2020 at 21:57):

The collection of linear combinations used to be called `lc`

but I think now it's just `finsupp`

#### Mario Carneiro (Jun 10 2020 at 21:58):

yeah it's `finsupp.mem_span_iff_total`

Last updated: May 07 2021 at 22:14 UTC