Zulip Chat Archive

Stream: Is there code for X?

Topic: Linear combination description of span

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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