hex

1.5. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexMatrixMathlib connects it to Mathlib: every Hex.Matrix corresponds to a Mathlib Matrix with the same entries.

🔗def
HexMatrixMathlib.matrixEquiv.{u_1} {R : Type u_1} {n m : ℕ} :
  Hex.Matrix R n m ≃ Matrix (Fin n) (Fin m) R
HexMatrixMathlib.matrixEquiv.{u_1}
  {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.

The Semiring, Ring, and Algebra structure on square matrices, and the One instance, are defined by transport through HexMatrixMathlib.matrixEquiv, bundled as HexMatrixMathlib.matrixRingEquiv and HexMatrixMathlib.matrixAlgEquiv. The elementary row operations become Mathlib's elementary matrices (HexMatrixMathlib.matrixEquiv_rowSwap, HexMatrixMathlib.matrixEquiv_rowScale, HexMatrixMathlib.matrixEquiv_rowAdd).