Correspondence lemmas carrying the executable container API of Hex.Matrix (transpose, row/column updates) across matrixEquiv to the matching Mathlib Matrix operations.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_transpose {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) : matrixEquiv M.transpose = (matrixEquiv M).transpose

Transpose commutes with matrixEquiv: the executable transpose becomes Mathlib's ᵀ.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_setRow {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) (dst : Fin n) (v : Vector R m) : matrixEquiv (M.setRow dst v) = (matrixEquiv M).updateRow dst (vectorEquiv v)

Replacing a row carries matrixEquiv to Mathlib's updateRow.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_setCol {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) (dst : Fin m) (v : Fin n → R) : matrixEquiv (M.setCol dst v) = (matrixEquiv M).updateCol dst v

Replacing a column carries matrixEquiv to Mathlib's updateCol.