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)

Compute row-span coefficients using Hex.Matrix.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

Soundness of Hex.Matrix.spanCoeffs: returned coefficients reconstruct the requested vector.

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

Decide row-span membership using Hex.Matrix.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

Hex.Matrix.spanContains is the Boolean isSome view of Hex.Matrix.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

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

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

Compute the nullspace basis using Hex.Matrix.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

The k-th column of Hex.Matrix.nullspaceBasisMatrix is the k-th vector in Hex.Matrix.nullspace.

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