Core dense matrix definitions for hex-matrix.

This module models matrices as Vector (Vector R m) n and provides the basic executable operations needed by later linear-algebra algorithms: row/column accessors, zero and identity matrices, dot products, matrix-vector multiplication, matrix-matrix multiplication, and norm-squared helpers.

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

Dense n × m matrices over R. Opaque one-field structure wrapping the row data; consumers go through rows/getRow/ofRows/ofFn and M[i] / M[(i,j)], never the data projection, so the representation can change later.

• ofRows :: (
• data : Vector (Vector R m) n

  Implementation detail — use Matrix.rows/getRow, never this projection.

• )

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 ⋯

@[implicit_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.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

@[implicit_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 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 reduce in the kernel. Compiled code runs the allocation-free Fin.foldl loop dotProductImpl via the @[csimp] below.

TODO: once https://github.com/leanprover/lean4/pull/14267 (make Fin.foldl reduce in the kernel) lands and this project's toolchain is bumped past it, collapse this reference/compiled split: define dotProduct directly as the native Fin.foldl loop and delete dotProductImpl and dotProduct_eq_impl. The native form will then kernel-reduce on its own, so the memLattice decide checks keep working without the List.finRange reference allocation.

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.

@[inline]

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. The only sanctioned way to observe the row data.

Equations

• M.rows = M.data

@[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.

Equations

• M.getRow i = M.rows[i]

@[implicit_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.rows[p.fst][p.snd] }

@[implicit_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.

Equations

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

@[implicit_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: for a future 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 }

@[implicit_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⟩ }

@[simp]

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

@[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 (so rows_* reduction lemmas fire on it in proofs).

@[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.

@[simp]

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

getRow on ofRows reduces to the underlying vector.

@[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, so proofs about the computable M[(i, j)] line up with the M[i][j] lemmas.

@[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).

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

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.

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.

Equations

• Hex.Matrix.ofFn f = { data := Vector.ofFn fun (i : Fin n) => Vector.ofFn fun (j : Fin m) => f i j }

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.

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.

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: destructuring consumes M, so the backing store is updated in place when M is unique.

Equations

• { data := d }.setRow dst v = { data := d.set (↑dst) v ⋯ }

@[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.

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 = { data := Vector.ofFn fun (j : Fin m) => M.col j }

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

@[implicit_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)]

@[implicit_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)]

@[implicit_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)]

@[implicit_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.

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

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 mul: transpose N once (turning its columns into contiguous rows), 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.ofFn fun (i : Fin n) (j : Fin k) => (M.row i).dotProduct (N.transpose.row j)

@[csimp]

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

@[implicit_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 }

@[implicit_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 }

@[implicit_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

@[implicit_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.

@[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

In-place modification of row i. Linear in M: destructuring consumes M, so when M is uniquely referenced the row is owned and Vector.modify updates the backing store without copying.

Equations

• { data := d }.modifyRow i f = { data := d.modify i f }

@[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 := d.swap i j hi hj }

@[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, in place when M is uniquely referenced.

Equations

• { data := d }.mapRows f = { data := Vector.map f d }

@[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

In-place 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, and each row update is in place when M is uniquely referenced (Vector.modify frees the row slot before applying f). This is the shared engine for the in-place column and diagonal scatters (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 via mapRowsIdx: each row's single dst entry is set, reusing the freed row slot, rather than rebuilding the whole matrix with ofFn.

Equations

• M.setCol dst v = M.mapRowsIdx fun (i : Fin n) (row : Vector R m) => row.set (↑dst) (v i) ⋯

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 via mapRowsIdx, analogous to setCol.

Equations

• M.modifyCol dst g = M.mapRowsIdx fun (i : Fin n) (row : Vector R m) => row.modify (↑dst) (g i)

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.

@[implicit_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 row data. The single sanctioned SMul instance for matrices: the Mathlib bridge layer reuses it rather than declaring its own, so there is no overlapping instance. Matches the action the former abbrev inherited from Vector, so c • M keeps its previous meaning.

Equations

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

@[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

@[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.