Stream: new members
Topic: Projection on basis
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
Alex J. Best (Aug 21 2020 at 14:13):
docs#is_basis.repr does what you want I think?
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.
Alex J. Best (Aug 21 2020 at 16:50):
Yeah I also found that docstring a little hard to understand.
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?
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