Stream: Is there code for X?
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.
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
Mario Carneiro (Jun 10 2020 at 21:58):
Last updated: May 07 2021 at 22:14 UTC