RCLike matrix as a family of vectors in the eulidean space

Stream: Is there code for X?

[nemo]

I want something like

Matrix.colVec {𝕜 : Type*} {m : Type*} {n : Type*} (A : Matrix m n 𝕜) :
  EuclideanSpace (EuclideanSpace 𝕜 m) n  := A.col

so that I can use the inner product and the L2-norm of two column vectors of A.

Is there code already existent for it?

[Eric Wieser]

That definition would be defeq abuse, you need to insert toLps to make that valid, something like toLp 2 (fun i => toLp 2 (A.col i))

[nemo]

Do you mean

def colVec (A : Matrix m n 𝕜) : EuclideanSpace (EuclideanSpace 𝕜 m) n :=
   WithLp.toLp 2 <| fun i => WithLp.toLp 2 <| A.col i

is more appropriate