def Hex.Matrix.IsRowReduced.pivotIndex? {R : Type u} {n m : Nat} (D : RowEchelonData R n m) (j : Fin m) : Option (Fin D.rank)

Find the pivot-row index for column j, if j is a pivot column.

Equations

• Hex.Matrix.IsRowReduced.pivotIndex? D j = Hex.Matrix.IsRowReduced.pivotIndexAux✝ D j 0 D.rank

def Hex.Matrix.IsRowReduced.nullspaceMatrix {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) : Matrix R m (m - D.rank)

Nullspace basis vectors assembled as columns indexed by the free variables.

Equations

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

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_free {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (k : Fin (m - D.rank)) : E.nullspaceMatrix[⋯.freeCols.get k][k] = 1

In the kth nullspace-matrix column, the row for its own free column is 1.

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_free_ne {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) {k l : Fin (m - D.rank)} (hkl : k ≠ l) : E.nullspaceMatrix[⋯.freeCols.get l][k] = 0

In the kth nullspace-matrix column, every other free-column row is 0.

theorem Hex.Matrix.IsRowReduced.nullspaceMatrix_pivot {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (i : Fin D.rank) (k : Fin (m - D.rank)) : E.nullspaceMatrix[D.pivotCols.get i][k] = -D.echelon[⋯.pivotRow i][⋯.freeCols.get k]

In a pivot-column row, a nullspace-matrix entry is the negative RREF entry in the matching pivot row and free column.

def Hex.Matrix.IsRowReduced.nullspace {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) : Vector (Vector R m) (m - D.rank)

The individual nullspace basis vectors.

Build the basis matrix once, then extract all of its columns. Keep nullspaceMatrix outside the per-column body so its free-column and pivot work remains shared.

Equations

• E.nullspace = Vector.ofFn fun (k : Fin (m - D.rank)) => E.nullspaceMatrix.col k

theorem Hex.Matrix.IsRowReduced.nullspace_get_free {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (k : Fin (m - D.rank)) : (E.nullspace.get k)[⋯.freeCols.get k] = 1

On its own free column, a nullspace basis vector has entry 1.

theorem Hex.Matrix.IsRowReduced.nullspace_get_free_ne {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) {k l : Fin (m - D.rank)} (hkl : k ≠ l) : (E.nullspace.get k)[⋯.freeCols.get l] = 0

On every other free column, a nullspace basis vector has entry 0.

theorem Hex.Matrix.IsRowReduced.nullspace_get_pivot {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] [Lean.Grind.Ring R] (E : M.IsRowReduced D) (i : Fin D.rank) (k : Fin (m - D.rank)) : (E.nullspace.get k)[D.pivotCols.get i] = -D.echelon[⋯.pivotRow i][⋯.freeCols.get k]

On a pivot column, a nullspace basis vector is the negative RREF entry in the matching pivot row and free column.

theorem Hex.Matrix.IsRowReduced.nullspace_sound {R : Type u} [Lean.Grind.Ring R] {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsRowReduced D) (k : Fin (m - D.rank)) : M * E.nullspace.get k = 0

Every basis vector returned by nullspace lies in the nullspace of M.

theorem Hex.Matrix.IsRowReduced.nullspace_complete {R : Type u} [Lean.Grind.Field R] {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsRowReduced D) (v : Vector R m) : M * v = 0 → ∃ (c : Vector R (m - D.rank)), E.nullspaceMatrix * c = v

Every nullspace vector is generated by the computed nullspace basis.