∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n), ((Matrix.toEuclideanLin M) v).ofLp = M.mulVec v.ofLp