Zulip Chat Archive

Stream: Is there code for X?

Topic: mem_span if finite linear combination


view this post on Zulip Johan Commelin (Feb 10 2020 at 09:21):

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?

view this post on Zulip Anne Baanen (Feb 10 2020 at 09:44):

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

view this post on Zulip Anne Baanen (Feb 10 2020 at 09:44):

Because I have no idea what that theorem states :P

view this post on Zulip Johan Commelin (Feb 10 2020 at 09:56):

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


Last updated: May 07 2021 at 18:19 UTC