Reshaping matrices

This defines the identitication between Mₙₓₘ(R) and Rⁿˣᵐ (see matrix.reshape), and shows some obvious properties of this identification.

def Matrix.reshape {R : Type u_1} {I : Type u_2} {J : Type u_3} [Semiring R] : Matrix I J R ≃ₗ[R] I × J → R

identifies matrices $M_{I\times J}(R)$ with $R^{I \times J}$, this is given by $\varrho (x)_{(i,j)} = x_{ij}$

Equations

• Matrix.reshape = (LinearEquiv.curry R R I J).symm

theorem Matrix.reshape_apply {R : Type u_3} {I : Type u_1} {J : Type u_2} [Semiring R] (x : Matrix I J R) (ij : I × J) : Matrix.reshape x ij = x ij.1 ij.2

theorem Matrix.reshape_symm_apply {R : Type u_3} {I : Type u_1} {J : Type u_2} [Semiring R] (x : I × J → R) (i : I) (j : J) : Matrix.reshape.symm x i j = x (i, j)

theorem Matrix.reshape_symm_apply' {R : Type u_3} {I : Type u_1} {J : Type u_2} [Semiring R] (x : I × J → R) (ij : I × J) : Matrix.reshape.symm x ij.1 ij.2 = x ij

theorem Matrix.reshape_one {R : Type u_2} {I : Type u_1} [Semiring R] [DecidableEq I] (x : I) (y : I) : Matrix.reshape 1 (x, y) = if x = y then 1 else 0

theorem Matrix.reshape_aux_star {R : Type u_1} {I : Type u_2} {J : Type u_3} [Semiring R] [Star R] (x : Matrix I J R) : star (Matrix.reshape x) = Matrix.reshape x.conj

${\varrho(x)}^*=\varrho(\bar{x})$