## Stream: new members

### Topic: reshaping matrices

#### Monica Omar (Feb 28 2023 at 16:02):

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 (Feb 28 2023 at 16:11):

docs#fin_prod_fin_equiv is probably the key piece here

#### Eric Wieser (Feb 28 2023 at 16:11):

Along with docs#linear_equiv.curry

#### Eric Wieser (Feb 28 2023 at 16:15):

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

#### Monica Omar (Feb 28 2023 at 16:18):

trying to define an identification for matrices with vectors

#### Eric Wieser (Feb 28 2023 at 16:19):

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

#### Eric Wieser (Feb 28 2023 at 16:20):

Monica Omar said:

trying to define an identification for matrices with vectors

what's the motivation for that?

Last updated: Dec 20 2023 at 11:08 UTC