Hi, I am looking for a lemma in mathcomp matrix libraries that allow me to express a vector in terms of a given set of basis vectors. Could someone please point me to the specific lemma that talks about such representation ? Thanks a lot ! :)

Well, there is no "lemma" per se for that, since if you have a basis expressed as a square matrix `P`

where each row represents a vector of the basis, and if you have a vector `v`

you want to reexpress in this basis, you only need to do `v * P^-1`

to get an row vector which represents the expression of `v`

in the basis `P`

.

Thanks Cyril ! I will try that.

is this really a MathComp analysis specific question? To me, it sounds like a general MathComp question (since basis vectors need not be of real numbers...)

yeah, it's a general Mathcomp question

This topic was moved here from #math-comp analysis > representation of a vector in terms of basis by Karl Palmskog

Last updated: Jan 29 2023 at 19:02 UTC