Projection on basis

Stream: new members

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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]

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

[Alex J. Best]

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]

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