Constructing a matrix from vectors

Stream: new members

[Michael Novak]

How can I construct a matrix whose columns or rows are given by some vectors?
For example if I have two vectors in the plane u, v : Fin 2 → ℝ how can I construct a 2x2 matrix whose columns or rows are the vectors u, v?

[Riccardo Brasca]

You can use Matrix.fromCols and friends.

[Riccardo Brasca]

As usual it depends on exactly you have the vectors, so maybe we need a #mwe.

[Michael Novak]

Well the minimal working example is pretty much:

import Mathlib

variable (u  v  :  Fin 2 → ℝ)

And then when I tried to do Matrix.fromCol u v it didn't really work

[Riccardo Brasca]

Do you want a Matrix (Fin 2) (Fin 2) ℝ?

[Michael Novak]

Could you explain the difference between a Matrix (Fin 2) (Fin 2) ℝ and Matrix 2 2 ℝ? I have to admit I don't really fully understand how matrices work in lean.

[Riccardo Brasca]

Have you tried to write Matrix 2 2 ℝ in Lean?

[Michael Novak]

No. It's my first time working with matrices.

[Riccardo Brasca]

Matrices are indexed by types, so Matrix 2 2 ℝ doesn't make sense. If you want what mathematically we call a "2x2 matrix" this is Matrix (Fin 2) (Fin 2) ℝ

[Riccardo Brasca]

It's a good idea to have a look through the library, at the beginning it can be a little painful, but one only has to get used to it.

[Michael Novak]

O.k, I thought about it a bit and I understand now. For some reason it didn't make sense to me that matrices are indexed by types, but actually it totally makes sense, just very different from what I am used to.

[Riccardo Brasca]

In your specific case you can do something like

import Mathlib

def foo (u v : Fin 2 → ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
  fun i j => if j = 0 then u i else v i

[Riccardo Brasca]

Using Matrix.fromCol should also be doable, somewhere we must have the equivalence between vectors and matrices over Unit.

[Michael Novak]

O.k, thank you very much!