Dense Row-Major Matrices

Basic dense row-major matrix storage, indexing, and homogeneous-system predicates.

def CompPoly.DenseMatrix.setD {alpha : Type u_1} (xs : Array alpha) (i : ℕ) (a : alpha) : Array alpha

Set an array entry when the index is in bounds; otherwise leave the array unchanged.

structure CompPoly.DenseMatrix (F : Type u_1) [Zero F] : Type u_1

A dense row-major matrix with dimensions stored explicitly.

• rows : ℕ
• cols : ℕ
• data : Array F

def CompPoly.DenseMatrix.WellFormed {F : Type u_1} [Zero F] (M : DenseMatrix F) : Prop

A dense matrix stores exactly one row-major entry for every matrix coordinate.

def CompPoly.DenseMatrix.index {F : Type u_1} [Zero F] (M : DenseMatrix F) (row col : ℕ) : ℕ

Row-major index for the matrix entry (row, col).

def CompPoly.DenseMatrix.get {F : Type u_1} [Zero F] (M : DenseMatrix F) (row col : ℕ) : F

Read a matrix entry, returning zero outside the stored data.

def CompPoly.DenseMatrix.set {F : Type u_1} [Zero F] (M : DenseMatrix F) (row col : ℕ) (value : F) : DenseMatrix F

Replace a matrix entry when the row-major slot is stored.

def CompPoly.DenseMatrix.ofFn {F : Type u_1} [Zero F] (rows cols : ℕ) (f : ℕ → ℕ → F) : DenseMatrix F

Construct a dense matrix from an entry function.

def CompPoly.DenseMatrix.dotRow {F : Type u_1} [Semiring F] (M : DenseMatrix F) (row : ℕ) (v : Array F) : F

Dot product of one matrix row with a vector.

def CompPoly.DenseMatrix.mulVec {F : Type u_1} [Semiring F] (M : DenseMatrix F) (v : Array F) : Array F

Matrix-vector product.

def CompPoly.DenseMatrix.VectorWidth {F : Type u_1} [Zero F] (M : DenseMatrix F) (v : Array F) : Prop

A vector has the same width as the matrix column count.

def CompPoly.DenseMatrix.NonzeroVector {F : Type u_1} [Zero F] (v : Array F) : Prop

A vector has at least one nonzero entry.

def CompPoly.DenseMatrix.IsHomogeneousSolution {F : Type u_1} [Semiring F] (M : DenseMatrix F) (v : Array F) : Prop

A vector solves the homogeneous system represented by M.