reshaping matrices

Stream: new members

[Monica Omar]

I'm trying to define a function for reshaping matrices, but got no clue how to do this (I gave an example of the map):

import linear_algebra.matrix.to_linear_equiv

variables {R : Type*} {n : ℕ} [ring R]

/--
  example:
    (11 12 ⋯ 1n       ( 11
      ⋮ ⋱    ⋮    ↦     12
      ⋮    ⋱            ⋮
     n1 n2 ⋯ nn)        1n
                        ⋮
                        n1
                        n2
                        ⋮
                        nn ) -/
def reshape : (matrix (fin n) (fin n) R) ≃ₗ[R] (fin (n ^ 2)) → R := sorry

[Eric Wieser]

docs#fin_prod_fin_equiv is probably the key piece here

[Eric Wieser]

Along with docs#linear_equiv.curry

[Eric Wieser]

What's the motivation here? This might be an #xy problem

[Monica Omar]

trying to define an identification for matrices with vectors

[Eric Wieser]

Then probably you want (matrix I J R) ≃ₗ[R] (I × J → R) := (linear_equiv.curry _ _).symm

[Eric Wieser]

Monica Omar said:

trying to define an identification for matrices with vectors

what's the motivation for that?