2.5. Recipes
These are how-to recipes for common tasks. Each executable recipe shows the idiomatic call and its result. Where a Mathlib correspondence theorem exists, a companion recipe shows how to prove the matching Mathlib fact by running the executable.
2.5.1. How to find a basis for the kernel of a matrix
You have a matrix over a field and want a basis for its kernel: the
vectors x with M * x = 0. Build the matrix with the #m[...]
literal. Hex.Matrix.nullspaceBasisMatrix returns the basis as
the columns of a matrix, one column per free (non-pivot) column of M.
open Hex Hex.Matrix
namespace HexRowReduceKernelRecipe
-- M has rank 1 (second row twice the first), 3 columns.
def M : Matrix Rat 2 3 := #m[1, 2, 3; 2, 4, 6]
-- The reduction reports rank 1, so nullity is 3 - 1 = 2.
#guard (Matrix.rowReduce M).rank = 1
-- The kernel basis, as the columns of a matrix.
#eval Matrix.nullspaceBasisMatrix M
-- The nullity is m - rank = 3 - 1 = 2.
#guard (Matrix.nullspace M).toArray.size = 2
end HexRowReduceKernelRecipe
Each column is a basis vector: the kernel is spanned by (-2, 1, 0) and
(-3, 0, 1). It is a genuine basis, not just a spanning set:
Hex.Matrix.nullspace_sound says each vector is annihilated by
M, and Hex.Matrix.nullspace_complete that every x with
M * x = 0 is a combination of them.
2.5.2. How to prove a fact about the Mathlib kernel by running Hex
Everything above is purely executable: #eval runs the Hex.Matrix
routines and reads back concrete numbers. This recipe crosses into
Mathlib. HexRowReduceMathlib proves the executable rank,
span, and nullspace agree with Mathlib's noncomputable Matrix.rank,
Submodule.span, and LinearMap.ker, so you can settle a Mathlib goal
by running the executable and rewriting through a correspondence
theorem.
For the rank, HexMatrixMathlib.rank_eq says the computed
Hex.Matrix.RowEchelonData.rank equals Matrix.rank (matrixEquiv M).
Rewriting with it turns a goal about the noncomputable Mathlib rank into
one about the executable rank, which the kernel evaluates directly.
open Hex Hex.Matrix HexMatrixMathlib
namespace HexRowReduceKernelProof
def A : _root_.Matrix (Fin 2) (Fin 3) Rat :=
!![1, 2, 3; 2, 4, 6]
theorem rank_eq_one : A.rank = 1 := ⊢ A.rank = 1
⊢ (matrixEquiv.symm A).rowReduce.rank = 1
All goals completed! 🐙
end HexRowReduceKernelProof
decide +kernel runs the row reduction in Lean's kernel and checks the
result. The proof depends only on propext, Classical.choice, and
Quot.sound, never the compiler-trusting native_decide (banned
project-wide). For the kernel as a subspace, the
same pattern uses HexMatrixMathlib.nullspace_span_eq_ker, whose
right-hand side is exactly the Mathlib LinearMap.ker of M's
mulVecLin.
2.5.3. How to test whether a vector is in the row span
You have a matrix and a vector and want to know whether the vector is a
linear combination of the rows. Hex.Matrix.spanContains is the
decidable test. Hex.Matrix.spanCoeffs returns the witnessing
coefficients when the answer is yes.
open Hex Hex.Matrix
namespace HexRowReduceSpanRecipe
def M : Matrix Rat 2 3 := #m[1, 2, 3; 2, 4, 6]
-- (1, 2, 3) is the first row, so it is in the row span.
#eval Matrix.spanContains M #v[1, 2, 3]
-- A vector off the rows' line is not.
#guard Matrix.spanContains M #v[1, 0, 0] = false
end HexRowReduceSpanRecipe
2.5.4. How to prove row-span membership in Mathlib by running Hex
The Mathlib-side companion, like the kernel proof above, crosses into
Mathlib. HexMatrixMathlib.spanContains_iff_mem_span turns the
executable Hex.Matrix.spanContains test into membership in
Mathlib's Submodule.span of the rows, so a Submodule.span goal is
proved the same way: rewrite through this theorem, then decide +kernel.
open Hex Hex.Matrix HexMatrixMathlib
namespace HexRowReduceSpanProof
def A : _root_.Matrix (Fin 2) (Fin 3) Rat :=
!![1, 2, 3; 2, 4, 6]
def w : Fin 3 → Rat := ![1, 2, 3]
theorem w_mem_span :
w ∈ Submodule.span Rat (Set.range A.row) := ⊢ w ∈ Submodule.span ℚ (Set.range A.row)
⊢ ⋯.spanContains (vectorEquiv.symm w) = true
All goals completed! 🐙
end HexRowReduceSpanProof