Converting matrix notation into function

Stream: new members

[Vivek Rajesh Joshi]

I've seen that Matrix.of can convert a function f : m -> n -> R into a 2D array. Is there anything that does the reverse? Given a 2D array, is there anything that turns it into a function as mentioned above?

[Yaël Dillies]

Just use the matrix as a function. There is a coercion from Matrix m n alpha to m -> n -> alpha

[Vivek Rajesh Joshi]

The listTransvecCol function is unable to accept the 2D array as a Matrix. Here's an mwe:

import Mathlib.Data.Matrix.Basis
import Mathlib.Data.Matrix.DMatrix
import Mathlib.LinearAlgebra.Matrix.Determinant
import Mathlib.LinearAlgebra.Matrix.Reindex
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Matrix.Notation

variable (n p : Type _) (R : Type u₂) {𝕜 : Type _} [Field 𝕜]

variable [DecidableEq n] [DecidableEq p]

variable [CommRing R]
variable {R n} (i j : n)

def transvection (c : R) : Matrix n n R :=
  1 + Matrix.stdBasisMatrix i j c

variable {r : ℕ} (M1 : Matrix (Fin (r+1)) (Fin (r+1)) 𝕜)

def listTransvecCol' : List (Matrix (Fin (r+1)) (Fin (r+1)) 𝕜) :=
  List.ofFn fun i : Fin r =>
    transvection (i) (r) <| -M1 (i) (r) / M1 (r) (r)

#eval listTransvecCol' !![1,2,3;4,5,6;7,8,9] (𝕜:=Rat)

(I've redefined listTransvecCol because I don't know how to define matrices with direct sum domains)
But when I define it as a function and explicitly state its type as Matrix (Fin 3) (Fin 3) Rat, it works:

def mat : (Matrix (Fin 3) (Fin 3) Rat)
| 0 => (fun x => x+1)
| 1 => (fun x => x+4)
| 2 => (fun x => x+7)
#eval listTransvecCol' mat

[Eric Wieser]

What's the error in your mwe? (Also note that without imports, it's not quite a mwe!)

[Vivek Rajesh Joshi]

Oops, sorry about that! I'll add the imports

[Vivek Rajesh Joshi]

Hmm, that's odd. Previously it was giving an error of something along the lines of "Expected type Matrix (Fin 3) (Fin 3) Rat but got type fun x => Matrix (Fin 3) (Fin 3) Rat". But now it's working fine. Thanks for the help anyways!