mem_span if finite linear combination

Stream: Is there code for X?

[Johan Commelin]

There used to be finsupp.mem_span_iff_total but with the refactor of basis and everything, I can't find something like it anymore. What I need is that every element of a span is a finite linear combination. What is the current mathlib way of writing this?

[Anne Baanen]

Is this different from the finsupp.mem_span_iff_totalstill available in linear_algebra/finsupp.lean?

[Anne Baanen]

Because I have no idea what that theorem states :P

[Johan Commelin]

Aah, awesome. No idea why my code search didn't find this.