hex

2.2. The echelon certificate🔗

The elementary row operations (Hex.Matrix.rowSwap, Hex.Matrix.rowScale, Hex.Matrix.rowAdd) are documented in HexMatrix. The Gauss-Jordan reduction in this chapter applies these operations to a matrix over a field.

An echelon computation returns a certificate of how it reduced: the rank, the reduced matrix, an invertible transform T with T * original = echelon, and each row's pivot column.

🔗structure
Hex.Matrix.RowEchelonData.{u} (R : Type u) (n m : ℕ) : Type u
Hex.Matrix.RowEchelonData.{u} (R : Type u)
  (n m : ℕ) : Type u

Pure data produced by an echelon-form algorithm.

Constructor

Hex.Matrix.RowEchelonData.mk.{u}

Fields

rank : ℕ

Number of pivots, i.e. the rank of the original matrix.

echelon : Hex.Matrix R n m

The matrix reduced to row-echelon form.

transform : Hex.Matrix R n n

The accumulated row-operation transform T with T * original = echelon.

pivotCols : Vector (Fin m) self.rank

Column index of each pivot, in increasing order.

Two predicates say when such a record is a genuine echelon or reduced-echelon form. Hex.Matrix.IsEchelonForm bundles the conditions any echelon form shares: the transform equation, the transform's invertibility, the rank bounds, and the staircase pivot structure. Hex.Matrix.IsRowReduced adds the two reduced-form conditions: each pivot is one, and every entry above a pivot is zero.