Array representation of matrices

This file relates Fin-indexed matrices to arrays of their entries in row-major ordering. This means that, for an m by n matrix, the entry at row i and column j can be found at index n * i + j in the array.

Main definitions

• Matrix.ofArray A h: The matrix with m rows and n columns whose entries are obtained from the array A of size m * n in row-major ordering.
• Matrix.toArray A: The array of entries of a matrix stored in row-major ordering.

Implementation notes

The index in the array is computed using Fin.mkDivMod so that Fin.divNat and Fin.modNat can be used to recover the matrix row and column from the array index.

def Matrix.ofArray {R : Type u_1} {m n : ℕ} (A : Array R) (hA : A.size = m * n) : Matrix (Fin m) (Fin n) R

Construct a matrix from an array in row-major ordering.

Equations

• Matrix.ofArray A hA i j = A[i.mkDivMod j]

@[simp]

theorem Matrix.ofArray_apply {R : Type u_1} {m n : ℕ} (A : Array R) (hA : A.size = m * n) (i : Fin m) (j : Fin n) : ofArray A hA i j = A[i.mkDivMod j]

@[simp]

theorem Matrix.ofArray_ofFn {R : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : ofArray (Array.ofFn fun (k : Fin (m * n)) => A k.divNat k.modNat) ⋯ = A

The matrix constructed from the row-major array of A's entries is A.

def Matrix.toArray {R : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : Array R

The array of the entries of a matrix in row-major ordering.

Equations

• A.toArray = Array.ofFn fun (k : Fin (m * n)) => A k.divNat k.modNat

@[simp]

theorem Matrix.size_toArray {R : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : A.toArray.size = m * n

@[simp]

theorem Matrix.ofArray_toArray {R : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : ofArray A.toArray ⋯ = A

@[simp]

theorem Matrix.toArray_ofArray {R : Type u_1} {m n : ℕ} (A : Array R) (hA : A.size = m * n) : (ofArray A hA).toArray = A

The row-major array of the matrix constructed from an array is that array.

theorem Matrix.ofArray_eq_of_getD {R : Type u_1} [Zero R] {m n : ℕ} (A : Array R) (hA : A.size = m * n) : ofArray A hA = of fun (i : Fin m) (j : Fin n) => A.getD (n * ↑i + ↑j) 0