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.
https://github.com/adamtopaz/mathlib/blob/lcspan/src/linear_algebra/lincomb.lean

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