theorem HexMatrixTheory.shape_iff (n m : ℕ) (rows : List (List ℤ)) : Hex.Matrix.Lists.shape n m rows = true ↔ rows.length = n ∧ ∀ row ∈ rows, row.length = m

theorem HexMatrixTheory.row_length {n m : ℕ} {rows : List (List ℤ)} (h : Hex.Matrix.Lists.shape n m rows = true) (i : Fin n) : (Hex.Matrix.Lists.entry [] rows ↑i).length = m

theorem HexMatrixTheory.dot_eq_sum (a b : List ℤ) : Hex.Matrix.Lists.dot a b = ∑ i : Fin a.length, a.getD (↑i) 0 * b.getD (↑i) 0

theorem HexMatrixTheory.ListProducts.column_getD (j : ℕ) (rows : List (List ℤ)) (i : ℕ) : (Hex.Matrix.Lists.column j rows).getD i 0 = (rows.getD i []).getD j 0

theorem HexMatrixTheory.mul_of_product {n k m : ℕ} {a b : List (List ℤ)} {c : ℕ → ℕ → ℤ} (ha : Hex.Matrix.Lists.shape n k a = true) (hc : Hex.Matrix.Lists.product n m a b c = true) : ofLists n k a * ofLists k m b = fun (i : Fin n) (j : Fin m) => c ↑i ↑j

Accepted list products give mathematical matrix products; decoding is used only by this theorem, outside the Boolean reduction path.

def HexMatrixTheory.matrixOfLists (n m : ℕ) (rows : List (List ℤ)) : Hex.Matrix ℤ n m

Decode lists to the executable matrix representation for reference certificate soundness. This definition is never reduced by a checker.

Equations

• HexMatrixTheory.matrixOfLists n m rows = HexMatrixTheory.matrixEquiv.symm (HexMatrixTheory.ofLists n m rows)

@[simp]

theorem HexMatrixTheory.matrixEquiv_matrixOfLists (n m : ℕ) (rows : List (List ℤ)) : matrixEquiv (matrixOfLists n m rows) = ofLists n m rows

theorem HexMatrixTheory.matrixOfLists_get (n m : ℕ) (rows : List (List ℤ)) (i : Fin n) (j : Fin m) : (matrixOfLists n m rows)[i][j] = Hex.Matrix.Lists.get rows ↑i ↑j

theorem HexMatrixTheory.matrix_mul_of_product {n k m : ℕ} {a b d : List (List ℤ)} (ha : Hex.Matrix.Lists.shape n k a = true) (h : Hex.Matrix.Lists.product n m a b (Hex.Matrix.Lists.get d) = true) : matrixOfLists n k a * matrixOfLists k m b = matrixOfLists n m d

theorem HexMatrixTheory.matrix_inverse_of_product {n : ℕ} {a b : List (List ℤ)} (ha : Hex.Matrix.Lists.shape n n a = true) (h : Hex.Matrix.Lists.product n n a b Hex.Matrix.Lists.identity = true) : matrixOfLists n n a * matrixOfLists n n b = Hex.Matrix.identity n