15.1. Introduction🔗

Released as hex-matrix, with the Mathlib correspondence in hex-matrix-mathlib.

Hex.Matrix R n m is an n × m matrix over R.

This library has the type, its arithmetic (the dot product, matrix-vector and matrix-matrix multiplication, transpose, the Gram matrix), and the elementary row and column operations. It depends only on HexBasic. The determinant, row reduction, and integer determinant are separate libraries built on it: HexDeterminant, HexRowReduce, HexBareiss.

The type and its operations are Mathlib-free. The last section connects them to Mathlib: the Semiring/Ring and One instances, and the identification with Mathlib's _root_.Matrix.