Public Matrix-level wrappers backed by the executable rowReduce: the row-span tests spanCoeffs/spanContains, the rank projection rowReduce_rank, and the nullspace basis nullspaceBasisMatrix/nullspace.

def Hex.Matrix.spanCoeffs {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : Option (Vector R n)

Convenience wrapper: compute row-span coefficients using rowReduce internally.

Equations

• M.spanCoeffs v = ⋯.spanCoeffs v

theorem Hex.Matrix.spanCoeffs_sound {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) (c : Vector R n) : M.spanCoeffs v = some c → vecMul c M = v

Wrapper-layer soundness contract for Matrix.spanCoeffs.

def Hex.Matrix.spanContains {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : Bool

Convenience wrapper: decide row-span membership using rowReduce internally.

Equations

• M.spanContains v = ⋯.spanContains v

@[simp]

theorem Hex.Matrix.spanContains_eq_isSome {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M.spanContains v = (M.spanCoeffs v).isSome

The public spanContains wrapper is the Boolean isSome view of spanCoeffs.

theorem Hex.Matrix.spanContains_iff {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M.spanContains v = true ↔ ∃ (c : Vector R n), vecMul c M = v

The public spanContains wrapper is exactly row-span membership.

theorem Hex.Matrix.spanCoeffs_eq_none_iff {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M.spanCoeffs v = none ↔ ¬∃ (c : Vector R n), vecMul c M = v

spanCoeffs returns none exactly when v is in no row combination of M, so a none result certifies that v is not in the row span.

def Hex.Matrix.rowReduce_rank {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : Nat

The rank returned by rowReduce.

Equations

• M.rowReduce_rank = M.rowReduce.rank

def Hex.Matrix.nullspaceBasisMatrix {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : Matrix R m (m - M.rowReduce_rank)

The public nullspace basis assembled as a matrix of basis columns.

Equations

• M.nullspaceBasisMatrix = ⋯.nullspaceMatrix

def Hex.Matrix.nullspace {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : Vector (Vector R m) (m - M.rowReduce_rank)

Convenience wrapper: compute the nullspace basis using rowReduce internally.

Equations

• M.nullspace = ⋯.nullspace

theorem Hex.Matrix.nullspaceBasisMatrix_col {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - M.rowReduce_rank)) : M.nullspaceBasisMatrix.col k = M.nullspace.get k

Public column bridge between the matrix and vector nullspace wrappers: the k-th column of nullspaceBasisMatrix M is the k-th vector in nullspace M.

theorem Hex.Matrix.nullspace_sound {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (k : Fin (m - M.rowReduce_rank)) : M * M.nullspace.get k = 0

Every vector returned by the public nullspace wrapper is annihilated by M.

theorem Hex.Matrix.nullspace_complete {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (v : Vector R m) : M * v = 0 → ∃ (c : Vector R (m - M.rowReduce_rank)), M.nullspaceBasisMatrix * c = v

Every vector annihilated by M is generated by the public nullspace basis matrix.