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.

Per-entry in place via Hex.Matrix.modifyEntries: each of the row's m entries is a single Vector.modify of the flat backing buffer, with no row materialization, when M is uniquely referenced.

Equations

• M.rowScale i c = M.modifyEntries ↑i fun (x : Fin m) (x_1 : R) => c * x_1

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 (one contiguous copy, a borrowed read taken before the write); the subsequent Hex.Matrix.modifyEntries then holds the only live reference to the buffer and updates the dst row's entries in place when the runtime sees it uniquely referenced, with no destination-row materialization.

Equations

• M.rowAdd src dst c = M.modifyEntries ↑dst fun (k : Fin m) (x : R) => x + 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.

The source column is read once into csrc (one contiguous copy, a borrowed read taken before the write); the subsequent modifyCol then holds the only live reference to the buffer and updates the dst column entry of each row in place — one single-entry Vector.modify of the flat buffer per row (O(n) writes total) — when the runtime sees it uniquely referenced, with no row materialization; the source column is first snapshotted into one owned O(n) vector via borrowed reads. This replaces the former mapRows pass, which materialized and reflattened every row.

Equations

• M.colAdd src dst c = M.modifyCol dst fun (i : Fin n) (x : R) => x + c * (M.col src)[i]

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, valid as a right-multiplication wrapper over a noncommutative ring. Same flat per-entry column engine as colAdd: read the source column once, then modifyCol the dst entries in place.

Equations

• M.colAddRight src dst c = M.modifyCol dst fun (i : Fin n) (x : R) => x + (M.col src)[i] * 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.

Both columns are read once (two borrowed O(n) reads taken before the writes), then written back with two Hex.Matrix.setCol passes that update one flat-buffer entry per row in place, reusing the backing store when M is uniquely referenced. This replaces the former Hex.Matrix.mapRows pass, which materialized and reflattened every row. The column mirror of Hex.Matrix.rowSwap.

Equations

• M.colSwap i j = (M.setCol i fun (r : Fin n) => (M.col j)[r]).setCol j fun (r : Fin n) => (M.col i)[r]

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