Zulip Chat Archive

Stream: new members

Topic: Projection on basis


view this post on Zulip Nicolò Cavalleri (Aug 21 2020 at 14:09):

I can't find in mathlib the name of the projection of a vector onto an element of the basis, i.e. the linear map that, given a basis, an element of the basis and a vector returns the component of the vector (I mean its value in the field) of that particular element. I looked everywhere in the file linear_algebra.basis but I did not find it: I do not want to assume the basis is orthonormal so the orthogonal projection does not work here

view this post on Zulip Alex J. Best (Aug 21 2020 at 14:13):

docs#is_basis.repr does what you want I think?

view this post on Zulip Nicolò Cavalleri (Aug 21 2020 at 16:50):

Yes thanks I actually saw it but I was confused by its description in the documentation in the top of the file and I did not recognize it. With the documentation you linked I think this is actually what I wanted even if I cannot really manage to use it.

view this post on Zulip Alex J. Best (Aug 21 2020 at 16:50):

Yeah I also found that docstring a little hard to understand.

view this post on Zulip Alex J. Best (Aug 21 2020 at 16:52):

What problems are you having using it? I guess you'll need to call it with a basis, a vector and then the index of the basis element you want?

view this post on Zulip Nicolò Cavalleri (Aug 21 2020 at 16:53):

Ok thanks I'm about to write my problem in the topic Basis dependence as it is related to both topics but I think more to that one


Last updated: May 16 2021 at 05:21 UTC