structure Hex.Matrix (R : Type u) (n m : Nat) : Type u

Dense n × m matrices over R, backed by a flat row-major buffer of the n * m entries: entry (i, j) is stored at flat index i * m + j. Opaque one-field structure; consumers go through rows/getRow/ofRows/ofFn and M[i] / M[(i,j)], never the data projection, so the representation can change.

• data : Vector R (n * m)

  Implementation detail — the flat row-major backing buffer. Use Matrix.rows/getRow, never this projection.

@[instance_reducible]

instance Hex.instDecidableEqMatrix {R✝ : Type u_1} {n✝ m✝ : Nat} [DecidableEq R✝] : DecidableEq (Matrix R✝ n✝ m✝)

Equations

• Hex.instDecidableEqMatrix = Hex.instDecidableEqMatrix.decEq

def Hex.instDecidableEqMatrix.decEq {R✝ : Type u_1} {n✝ m✝ : Nat} [DecidableEq R✝] (x✝ x✝¹ : Matrix R✝ n✝ m✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqMatrix.decEq { data := a } { data := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.instBEqMatrix {R✝ : Type u_1} {n✝ m✝ : Nat} [BEq R✝] : BEq (Matrix R✝ n✝ m✝)

Equations

• Hex.instBEqMatrix = { beq := Hex.instBEqMatrix.beq }

def Hex.instBEqMatrix.beq {R✝ : Type u_1} {n✝ m✝ : Nat} [BEq R✝] : Matrix R✝ n✝ m✝ → Matrix R✝ n✝ m✝ → Bool

Equations

• Hex.instBEqMatrix.beq { data := a } { data := b } = (a == b)
• Hex.instBEqMatrix.beq x✝¹ x✝ = false

noncomputable def Vector.dotProduct {R : Type u_1} {n : Nat} [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.

Equations

• u.dotProduct v = List.foldl (fun (acc : R) (i : Fin n) => acc + u[i] * v[i]) 0 (List.finRange n)

def Vector.dotProductImpl {R : Type u_1} {n : Nat} [Mul R] [Add R] [OfNat R 0] (u v : Vector R n) : R

Allocation-free implementation of dotProduct: a Fin.foldl loop that never materializes the List.finRange n index list. Swapped in for compiled code by the @[csimp] lemma; dotProduct remains the reference form for proofs.

Equations

• u.dotProductImpl v = Fin.foldl n (fun (acc : R) (i : Fin n) => acc + u[i] * v[i]) 0

@[csimp]

theorem Vector.dotProduct_eq_impl : @dotProduct = @dotProductImpl

def Vector.normSq {R : Type u_1} {n : Nat} [Mul R] [Add R] [OfNat R 0] (v : Vector R n) : R

Squared Euclidean norm of a vector.

Equations

• v.normSq = v.dotProduct v

def Vector.unit {n : Nat} (R : Type u) [Zero R] [One R] (i : Fin n) : Vector R n

The standard basis vector with value 1 at index i and 0 elsewhere.

Equations

• Vector.unit R i = Vector.ofFn fun (j : Fin n) => if i = j then One.one else Zero.zero

theorem Vector.getElem_unit {R : Type u_1} {n : Nat} [Zero R] [One R] (i j : Fin n) : (unit R i)[j] = if i = j then One.one else Zero.zero

Entry formula for a standard basis vector.

theorem Hex.Matrix.flatIdx_lt {n m i j : Nat} (hi : i < n) (hj : j < m) : i * m + j < n * m

The flat row-major index i * m + j of an in-range entry is in range.

theorem Hex.Matrix.flatIdx_div {i j m : Nat} (hj : j < m) : (i * m + j) / m = i

Recover the row index from a flat index: (i * m + j) / m = i when j < m.

theorem Hex.Matrix.flatIdx_mod {i j m : Nat} (hj : j < m) : (i * m + j) % m = j

Recover the column index from a flat index: (i * m + j) % m = j when j < m.

theorem Hex.Matrix.row_of_lt {n m : Nat} (p : Fin (n * m)) : ↑p / m < n

The row index recovered from any in-range flat index is in range.

theorem Hex.Matrix.col_of_lt {n m : Nat} (p : Fin (n * m)) : ↑p % m < m

The column index recovered from any in-range flat index is in range.

@[instance_reducible]

instance Hex.Matrix.instGetElemProdFinTrue {R : Type u} {n m : Nat} : GetElem (Matrix R n m) (Fin n × Fin m) R fun (x : Matrix R n m) (x_1 : Fin n × Fin m) => True

Entry access by a Fin n × Fin m index: the O(1) flat read.

Equations

• Hex.Matrix.instGetElemProdFinTrue = { getElem := fun (M : Hex.Matrix R n m) (p : Fin n × Fin m) (x : True) => M.data[↑p.fst * m + ↑p.snd] }

@[instance_reducible]

instance Hex.Matrix.instGetElemProdNatAndLtFstSnd {R : Type u} {n m : Nat} : GetElem (Matrix R n m) (Nat × Nat) R fun (x : Matrix R n m) (p : Nat × Nat) => p.fst < n ∧ p.snd < m

Entry access by a Nat × Nat index.

Equations

• Hex.Matrix.instGetElemProdNatAndLtFstSnd = { getElem := fun (M : Hex.Matrix R n m) (p : Nat × Nat) (h : p.fst < n ∧ p.snd < m) => M.data[p.fst * m + p.snd] }

@[inline]

def Hex.Matrix.getRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) : Vector R m

The i-th row of a matrix, materialized from the flat buffer. This copies the m contiguous entries of row i; it is the computable row accessor compiled code uses (single entries go through M[(i, j)], which does not materialize a row).

Equations

• M.getRow i = Vector.ofFn fun (j : Fin m) => M.data[↑i * m + ↑j]

@[instance_reducible]

noncomputable instance Hex.Matrix.instGetElemFinVectorTrue {R : Type u} {n m : Nat} : GetElem (Matrix R n m) (Fin n) (Vector R m) fun (x : Matrix R n m) (x_1 : Fin n) => True

Row access M[i] for i : Fin n. Deliberately noncomputable: with the flat (Vector R (n*m)) representation, materializing a whole row just to read it — and especially M[i][j] to read one entry — is the wrong cost model. This instance exists only so proofs may write M[i] / M[i][j]; executable code must use the computable getRow for rows and M[(i, j)] (O(1)) for single entries. Any compiled definition that reaches for M[i] will fail to compile, which is the intended guard.

Equations

• Hex.Matrix.instGetElemFinVectorTrue = { getElem := fun (M : Hex.Matrix R n m) (i : Fin n) (x : True) => M.getRow i }

@[instance_reducible]

noncomputable instance Hex.Matrix.instGetElemNatVectorLt {R : Type u} {n m : Nat} : GetElem (Matrix R n m) Nat (Vector R m) fun (x : Matrix R n m) (i : Nat) => i < n

Row access by a Nat index. Also noncomputable; see the Fin n instance.

Equations

• Hex.Matrix.instGetElemNatVectorLt = { getElem := fun (M : Hex.Matrix R n m) (i : Nat) (h : i < n) => M.getRow ⟨i, h⟩ }

def Hex.Matrix.rows {R : Type u} {n m : Nat} (M : Matrix R n m) : Vector (Vector R m) n

The rows of a matrix as a vector of row-vectors, materialized from the flat buffer. The only sanctioned way to observe the full row data; O(n * m).

Equations

• M.rows = Vector.ofFn fun (i : Fin n) => M.getRow i

def Hex.Matrix.ofRows {R : Type u} {n m : Nat} (v : Vector (Vector R m) n) : Matrix R n m

Build a matrix from a vector of its rows, flattening into the row-major backing buffer.

Equations

• Hex.Matrix.ofRows v = { data := Vector.ofFn fun (p : Fin (n * m)) => v[↑p / m][↑p % m] }

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

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

Equations

• Hex.Matrix.ofFn f = { data := Vector.ofFn fun (p : Fin (n * m)) => f ⟨↑p / m, ⋯⟩ ⟨↑p % m, ⋯⟩ }

@[simp]

theorem Hex.Matrix.getElem_eq_getRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) : M[i] = M.getRow i

Row access M[i] normalizes to the computable getRow M i.

@[simp]

theorem Hex.Matrix.getElem_nat_eq_getRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (h : i < n) : M[i] = M.getRow ⟨i, h⟩

Nat-indexed row access normalizes to getRow.

theorem Hex.Matrix.getElem_getRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) (j : Fin m) : (M.getRow i)[j] = M.data[↑i * m + ↑j]

Reading entry j of getRow M i is the flat read at i * m + j.

theorem Hex.Matrix.getElem_getRow_nat {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) {j : Nat} (hj : j < m) : (M.getRow i)[j] = M.data[↑i * m + j]

Nat-indexed form of getElem_getRow, for Vector.ext proofs.

@[simp]

theorem Hex.Matrix.getElem_pair_eq_nested {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) (j : Fin m) : M[(i, j)] = M[i][j]

The pair entry access (computable, O(1)) agrees with the nested row-then-element form. The nested form is the simp-normal form the entry lemmas are stated in.

@[simp]

theorem Hex.Matrix.getElem_pair_nat {R : Type u} {n m : Nat} (M : Matrix R n m) (p : Nat × Nat) (h : p.fst < n ∧ p.snd < m) : M[p] = M.rows[p.fst][p.snd]

Nat-pair entry access, normalized to the row lookup (concrete-index form). The statement observes rows, not the backing buffer, so it is representation- independent; the flat read behind it is getElem_pair_data below.

theorem Hex.Matrix.ext_data {R : Type u} {n m : Nat} {M N : Matrix R n m} (h : M.data = N.data) : M = N

Two matrices are equal when their flat backing buffers are equal.

theorem Hex.Matrix.ext_getElem {R : Type u} {n m : Nat} {M N : Matrix R n m} (h : ∀ (i : Fin n) (j : Fin m), M[i][j] = N[i][j]) : M = N

Two matrices are equal when they agree entrywise.

theorem Hex.Matrix.getElem_ofFn {R : Type u} {n m : Nat} (f : Fin n → Fin m → R) (i : Fin n) (j : Fin m) : (ofFn f)[i][j] = f i j

Entry access for a matrix built from an entry function.

@[simp]

theorem Hex.Matrix.getRow_ofRows {R : Type u} {n m : Nat} (v : Vector (Vector R m) n) (i : Fin n) : (ofRows v).getRow i = v[i]

getRow on ofRows reduces to the underlying vector.

theorem Hex.Matrix.getElem_ofRows {R : Type u} {n m : Nat} (v : Vector (Vector R m) n) (i : Fin n) (j : Fin m) : (ofRows v)[i][j] = v[i][j]

Entry access for a matrix built from a vector of rows.

@[simp]

theorem Hex.Matrix.rows_ofRows {R : Type u} {n m : Nat} (v : Vector (Vector R m) n) : (ofRows v).rows = v

theorem Hex.Matrix.ext {R : Type u} {n m : Nat} {M N : Matrix R n m} (h : M.rows = N.rows) : M = N

Two matrices are equal when their rows are equal.

theorem Hex.Matrix.ext_iff {R : Type u} {n m : Nat} {M N : Matrix R n m} : M = N ↔ M.rows = N.rows

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

The i-th row of a matrix.

Equations

• M.row i = M.getRow i

theorem Hex.Matrix.getElem_row {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) (j : Fin m) : (M.row i)[j] = M[i][j]

Entry access for a selected matrix row.

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

The j-th column of a matrix.

Equations

• M.col j = Vector.ofFn fun (i : Fin n) => M[(i, j)]

theorem Hex.Matrix.getElem_col {R : Type u} {n m : Nat} (M : Matrix R n m) (j : Fin m) (i : Fin n) : (M.col j)[i] = M[i][j]

Entry access for a selected matrix column.

@[inline]

def Hex.Matrix.writeRow {R : Type u} {n m : Nat} (d : Vector R (n * m)) (dst : Nat) (hdst : dst < n) (v : Vector R m) : Vector R (n * m)

Overwrite the m entries of row dst of the flat buffer d with the entries of v, in place when d is uniquely referenced.

Equations

• Hex.Matrix.writeRow d dst hdst v = Fin.foldl m (fun (d : Vector R (n * m)) (t : Fin m) => d.set (dst * m + ↑t) v[t] ⋯) d

def Hex.Matrix.setRow {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin n) (v : Vector R m) : Matrix R n m

Replace row dst of M with the vector v. Linear in M: the matrix is consumed, so the backing buffer is owned and writeRow updates it in place.

Equations

• { data := d }.setRow dst v = { data := Hex.Matrix.writeRow d ↑dst ⋯ v }

@[inline]

def Hex.Matrix.modifyRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (f : Vector R m → Vector R m) : Matrix R n m

Modification of row i. The matrix is consumed; the row is read out once (a borrowed read into a fresh m-vector, before the buffer is written), f is applied, and the result is written back through writeRow, in place when the runtime sees the buffer uniquely referenced at the write.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Hex.Matrix.swap {R : Type u} {n m : Nat} (M : Matrix R n m) (i j : Nat) (hi : i < n := by get_elem_tactic) (hj : j < n := by get_elem_tactic) : Matrix R n m

Swap rows i and j, in place when M is uniquely referenced.

Equations

• { data := d }.swap i j hi hj = { data := Fin.foldl m (fun (d : Vector R (n * m)) (t : Fin m) => d.swap (i * m + ↑t) (j * m + ↑t) ⋯ ⋯) d }

@[inline]

def Hex.Matrix.mapRows {R : Type u} {n m m' : Nat} (M : Matrix R n m) (f : Vector R m → Vector R m') : Matrix R n m'

Map a function over every row. The row width may change, so this materializes the rows, maps, and reflattens.

Equations

• M.mapRows f = Hex.Matrix.ofRows (Vector.map f M.rows)

@[simp]

theorem Hex.Matrix.getElem_rows {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (hi : i < n) : M.rows[i] = M.getRow ⟨i, hi⟩

Reading a row out of rows is getRow. The bridge between the Vector (Vector R m) n observation and the flat accessor.

theorem Hex.Matrix.foldl_set_ne {R : Type u} {m N : Nat} (idx : Fin m → Nat) (val : Fin m → R) (bd : ∀ (t : Fin m), idx t < N) {p : Nat} (hp : p < N) (xs : List (Fin m)) (d0 : Vector R N) : (∀ (t : Fin m), t ∈ xs → idx t ≠ p) → (List.foldl (fun (d : Vector R N) (t : Fin m) => d.set (idx t) (val t) ⋯) d0 xs)[p] = d0[p]

A left fold of per-index sets leaves untouched every position not among the written indices.

theorem Hex.Matrix.foldl_set_mem {R : Type u} {m N : Nat} (idx : Fin m → Nat) (val : Fin m → R) (bd : ∀ (t : Fin m), idx t < N) (hinj : ∀ (a b : Fin m), idx a = idx b → a = b) (xs : List (Fin m)) : xs.Nodup → ∀ (d0 : Vector R N) (r : Fin m), r ∈ xs → (List.foldl (fun (d : Vector R N) (t : Fin m) => d.set (idx t) (val t) ⋯) d0 xs)[idx r] = val r

A left fold of per-index sets at injectively-indexed positions over a Nodup list writes val r at position idx r for every member r.

theorem Hex.Matrix.nodup_finRange (k : Nat) : (List.finRange k).Nodup

List.finRange k has no repeated indices (core-only proof; the Batteries nodup_finRange is outside this Mathlib-free module's import closure).

theorem Hex.Matrix.getElem_writeRow {R : Type u} {n m : Nat} (d : Vector R (n * m)) (dst : Nat) (hdst : dst < n) (v : Vector R m) {r t : Nat} (hr : r < n) (ht : t < m) : (writeRow d dst hdst v)[r * m + t] = if r = dst then v[t] else d[r * m + t]

Entrywise read of writeRow: position (r, t) reads v[t] in the written row and the old buffer everywhere else.

@[simp]

theorem Hex.Matrix.rows_setRow {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin n) (v : Vector R m) : (M.setRow dst v).rows = M.rows.set (↑dst) v ⋯

theorem Hex.Matrix.setRow_get_self {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin n) (v : Vector R m) : (M.setRow dst v)[dst] = v

Reading back the replaced row dst of setRow M dst v yields v.

theorem Hex.Matrix.setRow_row_ne {R : Type u} {n m : Nat} (M : Matrix R n m) (dst r : Fin n) (v : Vector R m) (h : r ≠ dst) : (M.setRow dst v)[r] = M[r]

Replacing row dst leaves every other row unchanged.

@[inline]

def Hex.Matrix.modifyEntries {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (g : Fin m → R → R) : Matrix R n m

In-place per-entry update of row i: entry t becomes g t applied to its old value, written directly into the flat buffer with no row materialization. This is the per-entry engine the elementary row operations (rowScale, rowAdd) and the Bareiss row elimination build on: unlike modifyRow, whose whole-row function forces a row copy-out and copy-back, each entry here is a single in-place Vector.modify of the backing buffer when the matrix is uniquely referenced.

Equations

• { data := d }.modifyEntries i g = if h : i < n then { data := Fin.foldl m (fun (d : Vector R (n * m)) (t : Fin m) => d.modify (i * m + ↑t) (g t)) d } else { data := d }

theorem Hex.Matrix.getElem_modifyEntries {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (g : Fin m → R → R) (r : Fin n) (c : Fin m) : (M.modifyEntries i g)[r][c] = if ↑r = i then g c M[r][c] else M[r][c]

Entrywise read of modifyEntries: row i gets g applied entrywise, every other row is unchanged.

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

The transpose of a dense matrix.

Equations

• M.transpose = Hex.Matrix.ofFn fun (i : Fin m) (j : Fin n) => M[(j, i)]

theorem Hex.Matrix.getElem_transpose {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin m) (j : Fin n) : M.transpose[i][j] = M[j][i]

Entry access for the transpose of a dense matrix.

@[simp]

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

Transposing a dense matrix twice returns the original matrix.

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

The all-zero matrix.

Equations

• Hex.Matrix.zero n m = Hex.Matrix.ofFn fun (x : Fin n) (x_1 : Fin m) => 0

@[instance_reducible]

instance Hex.Matrix.instZeroOfOfNatOfNatNat {R : Type u} {n m : Nat} [OfNat R 0] : Zero (Matrix R n m)

Equations

• Hex.Matrix.instZeroOfOfNatOfNatNat = { zero := Hex.Matrix.zero n m }

theorem Hex.Matrix.getElem_zero {R : Type u} {n m : Nat} [OfNat R 0] (i : Fin n) (j : Fin m) : 0[i][j] = 0

Every entry of the zero matrix is 0.

@[simp]

theorem Hex.Matrix.row_zero {R : Type u} {n m : Nat} [OfNat R 0] (i : Fin n) : row 0 i = Vector.ofFn fun (x : Fin m) => 0

Every row of the zero matrix is the zero vector.

@[simp]

theorem Hex.Matrix.col_zero {R : Type u} {n m : Nat} [OfNat R 0] (j : Fin m) : col 0 j = Vector.ofFn fun (x : Fin n) => 0

Every column of the zero matrix is the zero vector.

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

The identity matrix.

Equations

• Hex.Matrix.identity n = Hex.Matrix.ofFn fun (i j : Fin n) => if i = j then 1 else 0

def Hex.Matrix.add {R : Type u} {n m : Nat} [Add R] (A B : Matrix R n m) : Matrix R n m

Entrywise matrix addition.

Equations

• A.add B = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin m) => A[(i, j)] + B[(i, j)]

@[instance_reducible]

instance Hex.Matrix.instAdd {R : Type u} {n m : Nat} [Add R] : Add (Matrix R n m)

Equations

• Hex.Matrix.instAdd = { add := Hex.Matrix.add }

def Hex.Matrix.neg {R : Type u} {n m : Nat} [Neg R] (A : Matrix R n m) : Matrix R n m

Entrywise matrix negation.

Equations

• A.neg = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin m) => -A[(i, j)]

@[instance_reducible]

instance Hex.Matrix.instNeg {R : Type u} {n m : Nat} [Neg R] : Neg (Matrix R n m)

Equations

• Hex.Matrix.instNeg = { neg := Hex.Matrix.neg }

def Hex.Matrix.sub {R : Type u} {n m : Nat} [Sub R] (A B : Matrix R n m) : Matrix R n m

Entrywise matrix subtraction.

Equations

• A.sub B = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin m) => A[(i, j)] - B[(i, j)]

@[instance_reducible]

instance Hex.Matrix.instSub {R : Type u} {n m : Nat} [Sub R] : Sub (Matrix R n m)

Equations

• Hex.Matrix.instSub = { sub := Hex.Matrix.sub }

theorem Hex.Matrix.getElem_add {R : Type u} {n m : Nat} [Add R] (A B : Matrix R n m) (i : Fin n) (j : Fin m) : (A + B)[i][j] = A[i][j] + B[i][j]

Entry access for matrix addition.

theorem Hex.Matrix.getElem_neg {R : Type u} {n m : Nat} [Neg R] (A : Matrix R n m) (i : Fin n) (j : Fin m) : (-A)[i][j] = -A[i][j]

Entry access for matrix negation.

theorem Hex.Matrix.getElem_sub {R : Type u} {n m : Nat} [Sub R] (A B : Matrix R n m) (i : Fin n) (j : Fin m) : (A - B)[i][j] = A[i][j] - B[i][j]

Entry access for matrix subtraction.

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

Multiply a matrix by a column vector.

Equations

• M.mulVec v = Vector.ofFn fun (i : Fin n) => (M.row i).dotProduct v

@[simp]

theorem Hex.Matrix.row_transpose {R : Type u} {n m : Nat} (M : Matrix R n m) (j : Fin m) : M.transpose.row j = M.col j

The j-th row of transpose M is the j-th column of M.

@[simp]

theorem Hex.Matrix.col_transpose {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) : M.transpose.col i = M.row i

The i-th column of transpose M is the i-th row of M.

noncomputable def Hex.Matrix.mul {R : Type u} {n m k : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (N : Matrix R m k) : 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.

Equations

• M.mul N = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin k) => (M.row i).dotProduct (N.col j)

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

Cache-friendly implementation of Hex.Matrix.mul: transpose N once (turning its columns into contiguous rows), materialize the transposed rows once, then take row-by-row dot products, so each column is built a single time rather than once per row of M. Swapped in for compiled code by the @[csimp] lemma; mul stays the column-based reference form for proofs.

Equations

• M.mulImpl N = Hex.Matrix.ofRows (Vector.ofFn fun (i : Fin n) => have ri := M.getRow i; Vector.ofFn fun (j : Fin k) => ri.dotProduct N.transpose.rows[j])

@[csimp]

theorem Hex.Matrix.mul_eq_mulImpl : @mul = @mulImpl

@[instance_reducible]

instance Hex.Matrix.instHMulVectorOfMulOfAddOfOfNatOfNatNat {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] : HMul (Matrix R n m) (Vector R m) (Vector R n)

Equations

• Hex.Matrix.instHMulVectorOfMulOfAddOfOfNatOfNatNat = { hMul := Hex.Matrix.mulVec }

@[instance_reducible]

instance Hex.Matrix.instHMulOfMulOfAddOfOfNatOfNatNat {R : Type u} {n m k : Nat} [Mul R] [Add R] [OfNat R 0] : HMul (Matrix R n m) (Matrix R m k) (Matrix R n k)

Equations

• Hex.Matrix.instHMulOfMulOfAddOfOfNatOfNatNat = { hMul := Hex.Matrix.mul }

@[instance_reducible]

instance Hex.Matrix.instMulOfAddOfOfNatOfNatNat {R : Type u} {n : Nat} [Mul R] [Add R] [OfNat R 0] : Mul (Matrix R n n)

Homogeneous multiplication on square matrices, agreeing with the heterogeneous HMul. This is the Mul instance Mathlib's Semiring/Ring structures build on; see HexMatrixMathlib.

Equations

• Hex.Matrix.instMulOfAddOfOfNatOfNatNat = { mul := Hex.Matrix.mul }

theorem Hex.Matrix.getElem_mulVec {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (v : Vector R m) (i : Fin n) : (M * v)[i] = (M.row i).dotProduct v

Entry characterization for matrix-vector multiplication.

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

Multiply a row vector by a matrix, v * M. Equal to transpose M * v; the j-th entry is ∑ i, M[i][j] * v[i], the combination of the rows of M with coefficients v.

Equations

• Hex.Matrix.vecMul v M = M.transpose * v

@[instance_reducible]

instance Hex.Matrix.instHMulVectorOfMulOfAddOfOfNatOfNatNat_1 {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] : HMul (Vector R n) (Matrix R n m) (Vector R m)

Equations

• Hex.Matrix.instHMulVectorOfMulOfAddOfOfNatOfNatNat_1 = { hMul := Hex.Matrix.vecMul }

theorem Hex.Matrix.getElem_vecMul {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (v : Vector R n) (M : Matrix R n m) (j : Fin m) : (v * M)[j] = (M.col j).dotProduct v

Entry characterization for vector-matrix multiplication.

theorem Hex.Matrix.getElem_mul {R : Type u} {n m k : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (N : Matrix R m k) (i : Fin n) (j : Fin k) : (M * N)[i][j] = (M.row i).dotProduct (N.col j)

Entry characterization for matrix multiplication.

@[simp]

theorem Hex.Matrix.row_mul {R : Type u} {n m k : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (N : Matrix R m k) (i : Fin n) : (M * N).row i = Vector.ofFn fun (j : Fin k) => (M.row i).dotProduct (N.col j)

Row i of M * N is the row of dot products of row M i against the columns of N.

@[simp]

theorem Hex.Matrix.col_mul {R : Type u} {n m k : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (N : Matrix R m k) (j : Fin k) : (M * N).col j = Vector.ofFn fun (i : Fin n) => (M.row i).dotProduct (N.col j)

Column j of M * N is the column of dot products of the rows of M against col N j.

theorem Hex.Matrix.getElem_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} (i j : Fin n) : (Matrix.identity n)[i][j] = if i = j then 1 else 0

The identity matrix entry function: (identity n)[i][j] = 1 if i = j, else 0.

@[simp]

theorem Hex.Matrix.transpose_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} : (Matrix.identity n).transpose = Matrix.identity n

The identity matrix is its own transpose.

@[simp]

theorem Hex.Matrix.row_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} (i : Fin n) : (Matrix.identity n).row i = Vector.ofFn fun (j : Fin n) => if i = j then 1 else 0

Row i of the identity matrix has a 1 in position i and 0 elsewhere.

@[simp]

theorem Hex.Matrix.col_identity {R : Type u} [OfNat R 0] [OfNat R 1] {n : Nat} (j : Fin n) : (Matrix.identity n).col j = Vector.ofFn fun (i : Fin n) => if i = j then 1 else 0

Column j of the identity matrix has a 1 in position j and 0 elsewhere.

@[simp]

theorem Hex.Matrix.rows_modifyRow {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (f : Vector R m → Vector R m) : (M.modifyRow i f).rows = M.rows.modify i f

@[simp]

theorem Hex.Matrix.getRow_modifyRow_self {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Fin n) (f : Vector R m → Vector R m) : (M.modifyRow (↑i) f).getRow i = f (M.getRow i)

Row i of modifyRow M i f is f applied to the old row i.

@[simp]

theorem Hex.Matrix.getRow_modifyRow_ne {R : Type u} {n m : Nat} (M : Matrix R n m) (i : Nat) (f : Vector R m → Vector R m) (j : Fin n) (h : i ≠ ↑j) : (M.modifyRow i f).getRow j = M.getRow j

Rows other than i are unchanged by modifyRow M i f.

@[simp]

theorem Hex.Matrix.rows_swap {R : Type u} {n m : Nat} (M : Matrix R n m) (i j : Nat) (hi : i < n) (hj : j < n) : (M.swap i j hi hj).rows = M.rows.swap i j hi hj

@[simp]

theorem Hex.Matrix.rows_mapRows {R : Type u} {n m m' : Nat} (M : Matrix R n m) (f : Vector R m → Vector R m') : (M.mapRows f).rows = Vector.map f M.rows

@[inline]

def Hex.Matrix.mapRowsIdx {R : Type u} {n m : Nat} (M : Matrix R n m) (f : Fin n → Vector R m → Vector R m) : Matrix R n m

Indexed row map: replace row i by f i (row i) for every i, threading M through a Fin.foldl of per-row modifyRows. No intermediate index list is allocated. The whole-row function forces each visited row to be materialized and written back (see modifyRow); per-entry updates should prefer the copy-free modifyEntries / setCol / modifyCol.

Equations

• M.mapRowsIdx f = Fin.foldl n (fun (M : Hex.Matrix R n m) (i : Fin n) => M.modifyRow (↑i) (f i)) M

theorem Hex.Matrix.rows_mapRowsIdx {R : Type u} {n m : Nat} (M : Matrix R n m) (f : Fin n → Vector R m → Vector R m) : (M.mapRowsIdx f).rows = Fin.foldl n (fun (d : Vector (Vector R m) n) (i : Fin n) => d.modify (↑i) (f i)) M.rows

The row data of mapRowsIdx is the corresponding Fin.foldl of Vector.modifys.

@[simp]

theorem Hex.Matrix.getRow_mapRowsIdx {R : Type u} {n m : Nat} (M : Matrix R n m) (f : Fin n → Vector R m → Vector R m) (r : Fin n) : (M.mapRowsIdx f).getRow r = f r (M.getRow r)

Row r of mapRowsIdx M f is f r applied to the original row r.

theorem Hex.Matrix.getElem_mapRowsIdx {R : Type u} {n m : Nat} (M : Matrix R n m) (f : Fin n → Vector R m → Vector R m) (r : Fin n) (c : Fin m) : (M.mapRowsIdx f)[r][c] = (f r (M.getRow r))[c]

Entry (r, c) of mapRowsIdx M f reads from the updated row f r (row r).

def Hex.Matrix.setCol {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) (v : Fin n → R) : Matrix R n m

Replace column dst of M with the entry function v. In place: one single-entry Vector.set of the flat buffer per row (O(n) writes total), reusing the backing store when M is uniquely referenced, rather than materializing any row or rebuilding the matrix.

Equations

• { data := d }.setCol dst v = { data := Fin.foldl n (fun (d : Vector R (n * m)) (i : Fin n) => d.set (↑i * m + ↑dst) (v i) ⋯) d }

theorem Hex.Matrix.getElem_setCol {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) (v : Fin n → R) (r : Fin n) (c : Fin m) : (M.setCol dst v)[r][c] = if c = dst then v r else M[r][c]

Entrywise characterization of setCol: the destination column is read from the replacement function and every other column is read from M.

@[simp]

theorem Hex.Matrix.setCol_self {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) : (M.setCol dst fun (r : Fin n) => M[r][dst]) = M

Replacing a column by itself leaves the matrix unchanged.

theorem Hex.Matrix.transpose_setRow {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin n) (v : Vector R m) : (M.setRow dst v).transpose = M.transpose.setCol dst fun (a : Fin m) => v[a]

Transposing a row replacement is a column replacement on the transpose: setRow on M corresponds to setCol on Mᵀ. This is the bridge the determinant row laws route through to reuse the column laws.

def Hex.Matrix.modifyCol {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) (g : Fin n → R → R) : Matrix R n m

In-place per-entry column modify: replace each entry M[i][dst] by g i M[i][dst], every other column unchanged. In place: one single-entry Vector.modify of the flat buffer per row, analogous to setCol.

Equations

• { data := d }.modifyCol dst g = { data := Fin.foldl n (fun (d : Vector R (n * m)) (i : Fin n) => d.modify (↑i * m + ↑dst) (g i)) d }

theorem Hex.Matrix.getElem_modifyCol {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) (g : Fin n → R → R) (r : Fin n) (c : Fin m) : (M.modifyCol dst g)[r][c] = if c = dst then g r M[r][dst] else M[r][c]

Entrywise characterization of modifyCol.

theorem Hex.Matrix.getElem_modifyCol_of_ne {R : Type u} {n m : Nat} (M : Matrix R n m) (dst : Fin m) (g : Fin n → R → R) (r : Fin n) {c : Fin m} (h : c ≠ dst) : (M.modifyCol dst g)[r][c] = M[r][c]

Entries outside column dst are unchanged by modifyCol.

@[instance_reducible]

instance Hex.Matrix.instSMul {R : Type u} {n m : Nat} {S : Type v} [SMul S R] : SMul S (Matrix R n m)

Scalar action on a matrix, delegated to the flat backing buffer. The single sanctioned SMul instance for matrices: the Mathlib bridge layer reuses it rather than declaring its own, so there is no overlapping instance.

Equations

• Hex.Matrix.instSMul = { smul := fun (c : S) (M : Hex.Matrix R n m) => { data := c • M.data } }

@[simp]

theorem Hex.Matrix.data_smul {R : Type u} {n m : Nat} {S : Type v} [SMul S R] (c : S) (M : Matrix R n m) : (c • M).data = c • M.data

@[simp]

theorem Hex.Matrix.smul_getElem {R : Type u} {n m : Nat} {S : Type v} [SMul S R] (c : S) (M : Matrix R n m) (i : Fin n) (j : Fin m) : (c • M)[i][j] = c • M[i][j]

Scalar action pushes through a nested entry read.

@[simp]

theorem Hex.Matrix.rows_smul {R : Type u} {n m : Nat} {S : Type v} [SMul S R] (c : S) (M : Matrix R n m) : (c • M).rows = c • M.rows