11.2. The dense matrix type🔗

This section is the definitions; the next section collects the theorems about them.

Hex.Matrix.ofFn builds a matrix from an entry function Fin n → Fin m → R. Hex.Matrix.row and Hex.Matrix.col return its rows and columns, and Hex.Matrix.transpose swaps them.

def

Hex.Matrix.ofFn.{u} {R : Type u} {n m : ℕ} (f : Fin n → Fin m → R) :
  Hex.Matrix R n m
Hex.Matrix.ofFn.{u} {R : Type u} {n m : ℕ}
  (f : Fin n → Fin m → R) :
  Hex.Matrix R n m

Build a matrix from an entry function, filling the flat backing buffer.

def

Hex.Matrix.row.{u} {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m)
  (i : Fin n) : Vector R m
Hex.Matrix.row.{u} {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) (i : Fin n) :
  Vector R m

The i-th row of a matrix.

def

Hex.Matrix.col.{u} {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m)
  (j : Fin m) : Vector R n
Hex.Matrix.col.{u} {R : Type u} {n m : ℕ}
  (M : Hex.Matrix R n m) (j : Fin m) :
  Vector R n

The j-th column of a matrix.

def

Hex.Matrix.transpose.{u} {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) :
  Hex.Matrix R m n
Hex.Matrix.transpose.{u} {R : Type u}
  {n m : ℕ} (M : Hex.Matrix R n m) :
  Hex.Matrix R m n

The transpose of a dense matrix.

The zero and identity matrices:

def

Hex.Matrix.zero.{u} {R : Type u} (n m : ℕ) [OfNat R 0] :
  Hex.Matrix R n m
Hex.Matrix.zero.{u} {R : Type u} (n m : ℕ)
  [OfNat R 0] : Hex.Matrix R n m

The all-zero matrix.

def

Hex.Matrix.identity.{u} {R : Type u} (n : ℕ) [OfNat R 0] [OfNat R 1] :
  Hex.Matrix R n n
Hex.Matrix.identity.{u} {R : Type u}
  (n : ℕ) [OfNat R 0] [OfNat R 1] :
  Hex.Matrix R n n

The identity matrix.

Matrix-vector and matrix-matrix multiplication are both written *. Each product entry is a row-by-column dot product.

def

Vector.dotProduct.{u_1} {R : Type u_1} {n : ℕ} [Mul R] [Add R]
  [OfNat R 0] (u v : Vector R n) : R
Vector.dotProduct.{u_1} {R : Type u_1}
  {n : ℕ} [Mul R] [Add R] [OfNat R 0]
  (u v : Vector R n) : R

Dot product of two vectors.

This List.finRange form is the reference definition the entry lemmas reason about; crucially it kernel-reduces, so #guard/decide checks over dotProduct (e.g. memLattice membership) stay evaluable — core Fin.foldl does not yet reduce in the kernel. Compiled code therefore uses the allocation-free Vector.dotProductImpl, selected by Vector.dotProduct_eq_impl, while logical evaluation retains the list-based form.

def

Hex.Matrix.mulVec.{u} {R : Type u} {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m) (v : Vector R m) : Vector R n
Hex.Matrix.mulVec.{u} {R : Type u}
  {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m)
  (v : Vector R m) : Vector R n

Multiply a matrix by a column vector.

def

Hex.Matrix.mul.{u} {R : Type u} {n m k : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m) (N : Hex.Matrix R m k) : Hex.Matrix R n k
Hex.Matrix.mul.{u} {R : Type u}
  {n m k : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m)
  (N : Hex.Matrix R m k) :
  Hex.Matrix R n k

Multiply two matrices, using the naive algorithm.

This reads each column col N j and is the reference definition the entry lemmas reason about. Compiled code uses the implementation below, which transposes N once so each column is materialized a single time instead of being rebuilt for every row of M; Hex.Matrix.mul_eq_impl selects Hex.Matrix.mulImpl for compiled code.

Strassen-Winograd multiplication, with a customizable base kernel for small sizes, is available as Hex.Matrix.mulStrassen, with equality proved by Hex.Matrix.mulStrassen_eq_mul. It cannot replace this definition through @[csimp]: the Winograd schedule subtracts blocks and therefore needs [Sub R], while naive multiplication does not. Callers over a ring opt into the Strassen-Winograd algorithm explicitly.

The Gram matrix of the rows and the leading principal submatrices used by the Bareiss recurrence:

def

Hex.Matrix.gramMatrix.{u_1} {R : Type u_1} {n m : ℕ} [Mul R] [Add R]
  [OfNat R 0] (M : Hex.Matrix R n m) : Hex.Matrix R n n
Hex.Matrix.gramMatrix.{u_1} {R : Type u_1}
  {n m : ℕ} [Mul R] [Add R] [OfNat R 0]
  (M : Hex.Matrix R n m) :
  Hex.Matrix R n n

Gram matrix of the rows of a dense matrix.

def

Hex.Matrix.principalSubmatrix.{u_1} {R : Type u_1} {n : ℕ}
  (M : Hex.Matrix R n n) (k : ℕ) (hk : k ≤ n) : Hex.Matrix R k k
Hex.Matrix.principalSubmatrix.{u_1}
  {R : Type u_1} {n : ℕ}
  (M : Hex.Matrix R n n) (k : ℕ)
  (hk : k ≤ n) : Hex.Matrix R k k

Leading principal k × k submatrix of a square matrix: the top-left block indexed by {0, …, k-1} along both axes. Includes the empty submatrix (k = 0) and is convenient for Bareiss pivot/minor statements.