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] :

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

Equations

theorem matrix.reshape_apply {R : Type u_1} {I : Type u_2} {J : Type u_3} [semiring R] (x : matrix I J R) (ij : I × J) :

theorem matrix.reshape_symm_apply {R : Type u_1} {I : Type u_2} {J : Type u_3} [semiring R] (x : I × J → R) (i : I) (j : J) :

theorem matrix.reshape_symm_apply' {R : Type u_1} {I : Type u_2} {J : Type u_3} [semiring R] (x : I × J → R) (ij : I × J) :

theorem matrix.reshape_one {R : Type u_1} {I : Type u_2} [semiring R] [decidable_eq I] (x y : I) :

theorem matrix.reshape_aux_star {R : Type u_1} {I : Type u_2} {J : Type u_3} [semiring R] [has_star R] (x : matrix I J R) :

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