transform type from a vector in R^n to a matrix of n by 1

Stream: mathlib4

[Chenyi Li]

In natural language, it is easy to see that any vectors in $\mathbb{R}^n$ is equivalent to a matrix of $\mathbb{R}^{n \times 1}$. However, things seem to be harder for me in mathlib4. If we have a vector v : EuclideanSpace ℝ (Fin n), how to tranform the type to a matrix with Matrix (Fin n) (Fin 1) ℝ. Is there any theorem in mathlib4 correlated to this problem? Thanks very much for your help!

[Adam Topaz]

You could uncurry and use an equiv on the indexing type, for example, but this is probably an #xy problem

[Fabrizio Barroero]

I am not sure this is what you are looking for, but you could have a look at Matrix.col.

Matrix.col u is the column matrix whose entries are given by u.