Elementary row and column operations.

This module contains the primitive executable row/column operations and their entrywise access lemmas. Algebraic preservation theorems for multiplication and inverse tracking live downstream in HexRowReduce.RowEchelon.

def Hex.Matrix.rowSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin n) : Matrix R n m

Swap rows i and j in a dense matrix.

Implemented with Vector.swap, which updates the dense backing store in place when M is uniquely referenced, rather than reading both rows and writing them back through two sets (which forces a copy of the outer vector).

Equations

• M.rowSwap i j = M.swap ↑i ↑j ⋯ ⋯

theorem Hex.Matrix.getElem_rowSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j r : Fin n) (k : Fin m) : (M.rowSwap i j)[r][k] = if r = j then M[i][k] else if r = i then M[j][k] else M[r][k]

Read an entry of rowSwap M i j by cases on the row index: row j returns the original row i, row i returns the original row j, and any other row is unchanged.

@[simp]

theorem Hex.Matrix.row_rowSwap_left {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin n) : (M.rowSwap i j).row i = M.row j

Row i of rowSwap M i j is the original row j.

@[simp]

theorem Hex.Matrix.row_rowSwap_right {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin n) : (M.rowSwap i j).row j = M.row i

Row j of rowSwap M i j is the original row i.

theorem Hex.Matrix.row_rowSwap_of_ne {R : Type u_1} {n m : Nat} (M : Matrix R n m) {i j r : Fin n} (hri : r ≠ i) (hrj : r ≠ j) : (M.rowSwap i j).row r = M.row r

Any row other than i and j is unchanged by rowSwap M i j.

theorem Hex.Matrix.rowSwap_diag_of_ne {R : Type u_1} {n : Nat} (M : Matrix R n n) {k pivot : Fin n} (h : pivot ≠ k) : (M.rowSwap k pivot)[k][k] = M[pivot][k]

Diagonal-entry corollary of getElem_rowSwap for square matrices: when pivot ≠ k, the (k, k) entry of rowSwap M k pivot is the original (pivot, k) entry.

def Hex.Matrix.rowScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (i : Fin n) (c : R) : Matrix R n m

Scale row i by c.

Vector.modify frees the row slot before applying the update, so when M is uniquely referenced both the outer vector and the row itself are updated in place: Vector.map reuses the freed row's backing store.

Equations

• M.rowScale i c = M.modifyRow ↑i fun (row : Vector R m) => Vector.map (fun (x : R) => c * x) row

theorem Hex.Matrix.getElem_rowScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (i r : Fin n) (c : R) (k : Fin m) : (M.rowScale i c)[r][k] = if r = i then c * M[i][k] else M[r][k]

Read an entry of rowScale M i c by cases on the row index: row i returns c * M[i][k], any other row is unchanged.

@[simp]

theorem Hex.Matrix.row_rowScale_self {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (i : Fin n) (c : R) : (M.rowScale i c).row i = Vector.ofFn fun (k : Fin m) => c * M[i][k]

Row i of rowScale M i c is the pointwise scalar multiple of row i.

theorem Hex.Matrix.row_rowScale_of_ne {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) {i r : Fin n} (c : R) (hri : r ≠ i) : (M.rowScale i c).row r = M.row r

Any row other than i is unchanged by rowScale M i c.

def Hex.Matrix.rowAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin n) (c : R) : Matrix R n m

Replace row dst by row dst + c * row src.

The source row is read once into rsrc, so the only remaining reference to M is the consuming Vector.modify, which updates the outer vector in place when M is uniquely referenced (dropping the old row dst). The replacement row is built fresh, since every entry of it changes.

Equations

• M.rowAdd src dst c = M.modifyRow ↑dst fun (rdst : Vector R m) => Vector.ofFn fun (k : Fin m) => rdst[k] + c * (M.getRow src)[k]

theorem Hex.Matrix.getElem_rowAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst r : Fin n) (c : R) (k : Fin m) : (M.rowAdd src dst c)[r][k] = if r = dst then M[dst][k] + c * M[src][k] else M[r][k]

Read an entry of rowAdd M src dst c by cases on the row index: row dst returns M[dst][k] + c * M[src][k], any other row is unchanged.

theorem Hex.Matrix.getElem_rowAdd_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin n} (c : R) (hsrcdst : src ≠ dst) (k : Fin m) : (M.rowAdd src dst c)[src][k] = M[src][k]

Source-row entries are unchanged by rowAdd M src dst c when src ≠ dst.

@[simp]

theorem Hex.Matrix.row_rowAdd_dst {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin n) (c : R) : (M.rowAdd src dst c).row dst = Vector.ofFn fun (k : Fin m) => M[dst][k] + c * M[src][k]

Row dst of rowAdd M src dst c is the pointwise row combination.

theorem Hex.Matrix.row_rowAdd_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src : Fin n) {dst r : Fin n} (c : R) (hrdst : r ≠ dst) : (M.rowAdd src dst c).row r = M.row r

Any row other than dst is unchanged by rowAdd M src dst c.

@[simp]

theorem Hex.Matrix.row_rowAdd_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin n} (c : R) (hsrcdst : src ≠ dst) : (M.rowAdd src dst c).row src = M.row src

The source row is unchanged by rowAdd M src dst c when src ≠ dst.

theorem Hex.Matrix.rowScale_eq_set {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (i : Fin n) (c : R) : M.rowScale i c = M.setRow i (Vector.ofFn fun (k : Fin m) => c * M[i][k])

rowScale as a single set of the scaled row. The executable definition goes through Vector.modify for in-place update; this is the value-level characterization for callers that reason about the result as a set.

theorem Hex.Matrix.rowAdd_eq_set {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin n) (c : R) : M.rowAdd src dst c = M.setRow dst (Vector.ofFn fun (k : Fin m) => M[dst][k] + c * M[src][k])

rowAdd as a single set of the combined row. The executable definition goes through Vector.modify for in-place update; this is the value-level characterization for callers that reason about the result as a set.

theorem Hex.Matrix.col_rowSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin n) (k : Fin m) : (M.rowSwap i j).col k = Vector.ofFn fun (r : Fin n) => if r = j then M[i][k] else if r = i then M[j][k] else M[r][k]

Column k of rowSwap M i j is column k of M with entries i and j exchanged.

theorem Hex.Matrix.col_rowScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (i : Fin n) (c : R) (k : Fin m) : (M.rowScale i c).col k = Vector.ofFn fun (r : Fin n) => if r = i then c * M[i][k] else M[r][k]

Column k of rowScale M i c is column k of M with entry i scaled by c.

theorem Hex.Matrix.col_rowAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin n) (c : R) (k : Fin m) : (M.rowAdd src dst c).col k = Vector.ofFn fun (r : Fin n) => if r = dst then M[dst][k] + c * M[src][k] else M[r][k]

Column k of rowAdd M src dst c is column k of M with the dst entry replaced by M[dst][k] + c * M[src][k].

def Hex.Matrix.colAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : Matrix R n m

Replace column dst by col dst + c * col src.

Rather than rebuilding the whole matrix with ofFn, each row is mapped to its update of the single dst entry. Vector.map frees each row slot before applying the function, so the outer vector is reused when M is uniquely referenced, and each row's single-entry update is itself in place when that row vector is uniquely referenced.

Equations

• M.colAdd src dst c = M.mapRows fun (row : Vector R m) => row.set (↑dst) (row[dst] + c * row[src]) ⋯

def Hex.Matrix.colAddRight {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : Matrix R n m

Replace column dst by col dst + col src * c.

This is the right-scalar variant of colAdd. It is the column-add operation whose right-multiplication wrapper is valid over a noncommutative ring.

Equations

• M.colAddRight src dst c = M.mapRows fun (row : Vector R m) => row.set (↑dst) (row[dst] + row[src] * c) ⋯

theorem Hex.Matrix.getElem_colAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) (j : Fin m) : (M.colAdd src dst c)[i][j] = if j = dst then M[i][j] + c * M[i][src] else M[i][j]

Read an entry of colAdd M src dst c by cases on the column index: column dst returns M[i][dst] + c * M[i][src], any other column is unchanged.

theorem Hex.Matrix.getElem_colAddRight {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) (j : Fin m) : (M.colAddRight src dst c)[i][j] = if j = dst then M[i][j] + M[i][src] * c else M[i][j]

Read an entry of colAddRight M src dst c by cases on the column index: column dst returns M[i][dst] + M[i][src] * c, any other column is unchanged.

@[simp]

theorem Hex.Matrix.col_colAdd_dst {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : (M.colAdd src dst c).col dst = Vector.ofFn fun (i : Fin n) => M[i][dst] + c * M[i][src]

Column dst of colAdd M src dst c is the pointwise column combination.

@[simp]

theorem Hex.Matrix.col_colAddRight_dst {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : (M.colAddRight src dst c).col dst = Vector.ofFn fun (i : Fin n) => M[i][dst] + M[i][src] * c

Column dst of colAddRight M src dst c is the pointwise column combination with right scalar multiplication.

theorem Hex.Matrix.col_colAdd_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src : Fin m) {dst j : Fin m} (c : R) (hjdst : j ≠ dst) : (M.colAdd src dst c).col j = M.col j

Any column other than dst is unchanged by colAdd M src dst c.

theorem Hex.Matrix.col_colAddRight_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src : Fin m) {dst j : Fin m} (c : R) (hjdst : j ≠ dst) : (M.colAddRight src dst c).col j = M.col j

Any column other than dst is unchanged by colAddRight M src dst c.

theorem Hex.Matrix.getElem_colAdd_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin m} (c : R) (hsrcdst : src ≠ dst) (i : Fin n) : (M.colAdd src dst c)[i][src] = M[i][src]

Source-column entries are unchanged by colAdd M src dst c when src ≠ dst.

theorem Hex.Matrix.getElem_colAddRight_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin m} (c : R) (hsrcdst : src ≠ dst) (i : Fin n) : (M.colAddRight src dst c)[i][src] = M[i][src]

Source-column entries are unchanged by colAddRight M src dst c when src ≠ dst.

@[simp]

theorem Hex.Matrix.col_colAdd_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin m} (c : R) (hsrcdst : src ≠ dst) : (M.colAdd src dst c).col src = M.col src

The source column is unchanged by colAdd M src dst c when src ≠ dst.

@[simp]

theorem Hex.Matrix.col_colAddRight_src_of_ne {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) {src dst : Fin m} (c : R) (hsrcdst : src ≠ dst) : (M.colAddRight src dst c).col src = M.col src

The source column is unchanged by colAddRight M src dst c when src ≠ dst.

theorem Hex.Matrix.row_colAdd {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) : (M.colAdd src dst c).row i = Vector.ofFn fun (j : Fin m) => if j = dst then M[i][j] + c * M[i][src] else M[i][j]

Row i of colAdd M src dst c is row i of M with the dst entry replaced by M[i][dst] + c * M[i][src].

theorem Hex.Matrix.row_colAddRight {R : Type u_1} {n m : Nat} [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) : (M.colAddRight src dst c).row i = Vector.ofFn fun (j : Fin m) => if j = dst then M[i][j] + M[i][src] * c else M[i][j]

Row i of colAddRight M src dst c is row i of M with the dst entry replaced by M[i][dst] + M[i][src] * c.

def Hex.Matrix.colSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) : Matrix R n m

Swap columns i and j in a dense matrix.

The swap is done row by row via mapRows: each row's i and j entries are exchanged with Vector.swap, reusing the freed row slot when M is uniquely referenced. The column mirror of rowSwap.

Equations

• M.colSwap i j = M.mapRows fun (row : Vector R m) => row.swap ↑i ↑j ⋯ ⋯

theorem Hex.Matrix.getElem_colSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) (r : Fin n) (c : Fin m) : (M.colSwap i j)[r][c] = if c = j then M[r][i] else if c = i then M[r][j] else M[r][c]

Read an entry of colSwap M i j by cases on the column index: column j returns the original column i, column i returns the original column j, and any other column is unchanged.

@[simp]

theorem Hex.Matrix.col_colSwap_left {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) : (M.colSwap i j).col i = M.col j

Column i of colSwap M i j is the original column j.

@[simp]

theorem Hex.Matrix.col_colSwap_right {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) : (M.colSwap i j).col j = M.col i

Column j of colSwap M i j is the original column i.

theorem Hex.Matrix.col_colSwap_of_ne {R : Type u_1} {n m : Nat} (M : Matrix R n m) {i j c : Fin m} (hci : c ≠ i) (hcj : c ≠ j) : (M.colSwap i j).col c = M.col c

Any column other than i and j is unchanged by colSwap M i j.

theorem Hex.Matrix.row_colSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) (r : Fin n) : (M.colSwap i j).row r = Vector.ofFn fun (c : Fin m) => if c = j then M[r][i] else if c = i then M[r][j] else M[r][c]

Row r of colSwap M i j is row r of M with entries i and j exchanged.

theorem Hex.Matrix.transpose_colSwap {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i j : Fin m) : (M.colSwap i j).transpose = M.transpose.rowSwap i j

Transposing a column swap is the corresponding row swap on the transpose. This is the bridge the determinant column laws route through.

def Hex.Matrix.colScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (j : Fin m) (c : R) : Matrix R n m

Scale column j by c.

In-place per-entry column update via modifyCol: each row's single j entry is multiplied by c, reusing the freed row slot when M is uniquely referenced. The column mirror of rowScale.

Equations

• M.colScale j c = M.modifyCol j fun (x : Fin n) (x_1 : R) => c * x_1

theorem Hex.Matrix.getElem_colScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (j : Fin m) (c : R) (r : Fin n) (k : Fin m) : (M.colScale j c)[r][k] = if k = j then c * M[r][j] else M[r][k]

Read an entry of colScale M j c by cases on the column index: column j returns c * M[r][j], any other column is unchanged.

@[simp]

theorem Hex.Matrix.col_colScale_self {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (j : Fin m) (c : R) : (M.colScale j c).col j = Vector.ofFn fun (i : Fin n) => c * M[i][j]

Column j of colScale M j c is the pointwise scalar multiple of column j.

theorem Hex.Matrix.col_colScale_of_ne {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) {j k : Fin m} (c : R) (hkj : k ≠ j) : (M.colScale j c).col k = M.col k

Any column other than j is unchanged by colScale M j c.

theorem Hex.Matrix.row_colScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (j : Fin m) (c : R) (r : Fin n) : (M.colScale j c).row r = Vector.ofFn fun (k : Fin m) => if k = j then c * M[r][j] else M[r][k]

Row r of colScale M j c is row r of M with entry j scaled by c.

theorem Hex.Matrix.transpose_colScale {R : Type u_1} {n m : Nat} [Mul R] (M : Matrix R n m) (j : Fin m) (c : R) : (M.colScale j c).transpose = M.transpose.rowScale j c

Transposing a column scaling is the corresponding row scaling on the transpose.