Identification lemmas between Hex.Matrix and Mathlib's Matrix.

This module exposes a concrete equivalence between the dense executable Vector-based matrix representation used by HexMatrix and Mathlib's function-based Matrix, together with the first row-operation correspondence lemmas needed by downstream determinant and rank lemmas.

def HexMatrixMathlib.matrixEquiv {R : Type u_1} {n m : ℕ} : Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R

The bijection between a Hex.Matrix and the Mathlib Matrix with the same entries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_apply {R : Type u_1} {n m : ℕ} (M : Hex.Matrix R n m) (i : Fin n) (j : Fin m) : matrixEquiv M i j = M[i][j]

matrixEquiv M has entry M[i][j] at (i, j), so a caller can rewrite matrixEquiv M i j to M[i][j] without unfolding the equivalence.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_symm_apply {n m : ℕ} {R : Type u_1} (M : Matrix (Fin n) (Fin m) R) (i : Fin n) (j : Fin m) : (matrixEquiv.symm M)[↑i][↑j] = M i j

The inverse direction of matrixEquiv materialises a Mathlib matrix as an executable one entrywise: (matrixEquiv.symm M)[i][j] is just M i j.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_ofFn {n m : ℕ} {R : Type u_1} (f : Fin n → Fin m → R) : matrixEquiv (Hex.Matrix.ofFn f) = f

matrixEquiv is a left inverse of Hex.Matrix.ofFn: building an executable matrix from f and transporting it to Mathlib recovers f itself.

theorem HexMatrixMathlib.matrixEquiv_rowSwap {R : Type u_1} [Semiring R] {n m : ℕ} (M : Hex.Matrix R n m) (i j : Fin n) : matrixEquiv (M.rowSwap i j) = Matrix.swap R i j * matrixEquiv M

The executable elementary row swap corresponds to left multiplication by Mathlib's permutation matrix Matrix.swap, so downstream determinant and rank lemmas can reason about rowSwap through Mathlib's swap algebra.

theorem HexMatrixMathlib.matrixEquiv_rowScale {R : Type u_1} [Semiring R] {n m : ℕ} (M : Hex.Matrix R n m) (i : Fin n) (c : R) : matrixEquiv (M.rowScale i c) = Matrix.diagonal (Function.update (fun (x : Fin n) => 1) i c) * matrixEquiv M

The executable elementary row scaling corresponds to left multiplication by the diagonal matrix that carries c in row i and 1 elsewhere, exposing rowScale to Mathlib's diagonal-matrix algebra.

theorem HexMatrixMathlib.matrixEquiv_rowAdd {R : Type u_1} [CommRing R] {n m : ℕ} (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : matrixEquiv (M.rowAdd src dst c) = Matrix.transvection dst src c * matrixEquiv M

The executable elementary row addition (add c times row src to row dst) corresponds to left multiplication by Mathlib's transvection matrix, completing the row-operation dictionary used by the determinant correspondence.