hex

1.2. The dense matrix type🔗

Hex.Matrix.ofFn builds a matrix from an entry function Fin n → Fin m → R. row and col return its rows and columns, and 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.

🔗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.

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

Transposing a dense matrix twice returns the original 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; compiled code runs the allocation-free Fin.foldl loop dotProductImpl via the @[csimp] below.

🔗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 runs mulImpl, which transposes N once (via the @[csimp] below) so each column is materialized a single time instead of being rebuilt for every row of M.

We intend to provide Strassen-Winograd with a customizable algorithm for small sizes later.

The identity is a left and right unit, and multiplication is associative.

🔗theorem
Hex.Matrix.identity_mul.{u_1} {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R] (M : Hex.Matrix R n m) :
  Hex.Matrix.identity n * M = M
Hex.Matrix.identity_mul.{u_1}
  {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R]
  (M : Hex.Matrix R n m) :
  Hex.Matrix.identity n * M = M

Left-multiplication by the identity matrix leaves a matrix unchanged.

🔗theorem
Hex.Matrix.mul_identity.{u_1} {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R] (M : Hex.Matrix R n m) :
  M * Hex.Matrix.identity m = M
Hex.Matrix.mul_identity.{u_1}
  {R : Type u_1} {n m : ℕ}
  [Lean.Grind.Ring R]
  (M : Hex.Matrix R n m) :
  M * Hex.Matrix.identity m = M

Right-multiplication by the identity matrix leaves a matrix unchanged.

🔗theorem
Hex.Matrix.mul_assoc.{u_1} {R : Type u_1} {n m k l : ℕ}
  [Lean.Grind.Ring R] (A : Hex.Matrix R n m) (B : Hex.Matrix R m k)
  (C : Hex.Matrix R k l) : A * B * C = A * (B * C)
Hex.Matrix.mul_assoc.{u_1} {R : Type u_1}
  {n m k l : ℕ} [Lean.Grind.Ring R]
  (A : Hex.Matrix R n m)
  (B : Hex.Matrix R m k)
  (C : Hex.Matrix R k l) :
  A * B * C = A * (B * C)

Matrix multiplication is associative.

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.