Algebraic properties of elementary row/column operations.

The primitive executable operations live in HexMatrix.Elementary. This module adds the multiplication- and inverse-preservation facts (rowSwap_mul, rowScale_mul, rowAdd_mul, the *_transform_mul_preserve and *_inverse_preserve families, and the column-operation analogues) on which the row-reduction, span/nullspace, and determinant routines rely.

theorem Hex.Matrix.rowSwap_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (i j : Fin n) : A.rowSwap i j * B = (A * B).rowSwap i j

Multiplication by B commutes with row swap on the left factor.

theorem Hex.Matrix.rowScale_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (i : Fin n) (s : R) : A.rowScale i s * B = (A * B).rowScale i s

Multiplication by B commutes with row scaling on the left factor.

theorem Hex.Matrix.rowAdd_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (src dst : Fin n) (s : R) : A.rowAdd src dst s * B = (A * B).rowAdd src dst s

Multiplication by B commutes with the row-add operation on the left factor.

theorem Hex.Matrix.rowSwap_mulVec_getElem {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (v : Vector R m) (i j r : Fin n) : (M.rowSwap i j * v)[r] = if r = j then (M * v)[i] else if r = i then (M * v)[j] else (M * v)[r]

Entrywise action of row swap on matrix-vector multiplication.

theorem Hex.Matrix.rowScale_mulVec_getElem {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) (v : Vector R m) (i r : Fin n) (s : R) : (M.rowScale i s * v)[r] = if r = i then s * (M * v)[i] else (M * v)[r]

Entrywise action of row scaling on matrix-vector multiplication.

theorem Hex.Matrix.rowAdd_mulVec_getElem {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) (v : Vector R m) (src dst r : Fin n) (s : R) : (M.rowAdd src dst s * v)[r] = if r = dst then (M * v)[dst] + s * (M * v)[src] else (M * v)[r]

Entrywise action of row addition on matrix-vector multiplication.

theorem Hex.Matrix.rowSwap_transform_mul_preserve {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] {T : Matrix R n n} {M E : Matrix R n m} (i j : Fin n) (h : T * M = E) : T.rowSwap i j * M = E.rowSwap i j

If T * M = E, then rowSwap T i j * M = rowSwap E i j: row swap on the transform side preserves the equation T * M = E when applied to both T and E.

theorem Hex.Matrix.rowScale_transform_mul_preserve {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] {T : Matrix R n n} {M E : Matrix R n m} (i : Fin n) (s : R) (h : T * M = E) : T.rowScale i s * M = E.rowScale i s

If T * M = E, then rowScale T i s * M = rowScale E i s: row scale on the transform side preserves the equation T * M = E when applied to both T and E.

theorem Hex.Matrix.rowAdd_transform_mul_preserve {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] {T : Matrix R n n} {M E : Matrix R n m} (src dst : Fin n) (s : R) (h : T * M = E) : T.rowAdd src dst s * M = E.rowAdd src dst s

If T * M = E, then rowAdd T src dst s * M = rowAdd E src dst s: row add on the transform side preserves the equation T * M = E when applied to both T and E.

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

Swapping the same two rows twice restores the original matrix.

@[simp]

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

Swapping a row with itself leaves the matrix unchanged.

@[simp]

theorem Hex.Matrix.rowScale_one {R : Type u_1} {n m : Nat} [Lean.Grind.Semiring R] (M : Matrix R n m) (i : Fin n) : M.rowScale i 1 = M

Scaling a row by one leaves the matrix unchanged.

@[simp]

theorem Hex.Matrix.rowAdd_zero {R : Type u_1} {n m : Nat} [Lean.Grind.Semiring R] (M : Matrix R n m) (src dst : Fin n) : M.rowAdd src dst 0 = M

Adding zero times one row to another leaves the matrix unchanged.

theorem Hex.Matrix.rowScale_rowScale_inv_left {R : Type u_1} {n m : Nat} [Lean.Grind.Field R] (M : Matrix R n m) (i : Fin n) {s : R} (hs : s ≠ 0) : (M.rowScale i s).rowScale i s⁻¹ = M

Scaling a row by s and then by s⁻¹ restores the original matrix when s is nonzero.

theorem Hex.Matrix.rowScale_rowScale_inv_right {R : Type u_1} {n m : Nat} [Lean.Grind.Field R] (M : Matrix R n m) (i : Fin n) {s : R} (hs : s ≠ 0) : (M.rowScale i s⁻¹).rowScale i s = M

Scaling a row by s⁻¹ and then by s restores the original matrix when s is nonzero.

theorem Hex.Matrix.rowAdd_rowAdd_neg {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) {src dst : Fin n} (s : R) (hsrcdst : src ≠ dst) : (M.rowAdd src dst s).rowAdd src dst (-s) = M

Adding s times a distinct source row to a destination row and then adding -s times that source row restores the original matrix.

theorem Hex.Matrix.rowAdd_rowAdd_neg_left {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) {src dst : Fin n} (s : R) (hsrcdst : src ≠ dst) : (M.rowAdd src dst (-s)).rowAdd src dst s = M

Adding -s times a distinct source row to a destination row and then adding s times that source row restores the original matrix.

theorem Hex.Matrix.rowSwap_left_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (T : Matrix R n n) (i j : Fin n) (hT : ∃ (Tinv : Matrix R n n), Tinv * T = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), Tinv' * T.rowSwap i j = Matrix.identity n

A row swap preserves existence of a left inverse for a row transform.

theorem Hex.Matrix.rowSwap_right_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (T : Matrix R n n) (i j : Fin n) (hT : ∃ (Tinv : Matrix R n n), T * Tinv = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), T.rowSwap i j * Tinv' = Matrix.identity n

A row swap preserves existence of a right inverse for a row transform.

theorem Hex.Matrix.rowScale_left_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Field R] (T : Matrix R n n) (i : Fin n) {s : R} (hs : s ≠ 0) (hT : ∃ (Tinv : Matrix R n n), Tinv * T = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), Tinv' * T.rowScale i s = Matrix.identity n

Scaling a row by a nonzero scalar preserves existence of a left inverse for a row transform.

theorem Hex.Matrix.rowScale_right_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Field R] (T : Matrix R n n) (i : Fin n) {s : R} (hs : s ≠ 0) (hT : ∃ (Tinv : Matrix R n n), T * Tinv = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), T.rowScale i s * Tinv' = Matrix.identity n

Scaling a row by a nonzero scalar preserves existence of a right inverse for a row transform.

theorem Hex.Matrix.rowAdd_left_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (T : Matrix R n n) {src dst : Fin n} (s : R) (hsrcdst : src ≠ dst) (hT : ∃ (Tinv : Matrix R n n), Tinv * T = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), Tinv' * T.rowAdd src dst s = Matrix.identity n

Adding a multiple of a distinct source row preserves existence of a left inverse for a row transform.

theorem Hex.Matrix.rowAdd_right_inverse_preserve {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (T : Matrix R n n) {src dst : Fin n} (s : R) (hsrcdst : src ≠ dst) (hT : ∃ (Tinv : Matrix R n n), T * Tinv = Matrix.identity n) : ∃ (Tinv' : Matrix R n n), T.rowAdd src dst s * Tinv' = Matrix.identity n

Adding a multiple of a distinct source row preserves existence of a right inverse for a row transform.

theorem Hex.Matrix.mul_colAdd {R : Type u_1} {n m k : Nat} [Lean.Grind.CommRing R] (A : Matrix R n m) (B : Matrix R m k) (src dst : Fin k) (s : R) : A * B.colAdd src dst s = (A * B).colAdd src dst s

Multiplication by A commutes with the column-add operation on the right factor over commutative rings.

theorem Hex.Matrix.mul_colAddRight {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (src dst : Fin k) (s : R) : A * B.colAddRight src dst s = (A * B).colAddRight src dst s

Right multiplication by a right-scalar column addition commutes with the column-add operation over a possibly noncommutative ring.

@[simp]

theorem Hex.Matrix.colAdd_zero {R : Type u_1} {n m : Nat} [Lean.Grind.Semiring R] (M : Matrix R n m) (src dst : Fin m) : M.colAdd src dst 0 = M

Adding zero times one column to another leaves the matrix unchanged.

@[simp]

theorem Hex.Matrix.colAddRight_zero {R : Type u_1} {n m : Nat} [Lean.Grind.Semiring R] (M : Matrix R n m) (src dst : Fin m) : M.colAddRight src dst 0 = M

Adding one column times zero to another leaves the matrix unchanged.