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

Reduced row echelon form data computed by Gauss-Jordan elimination.

Equations

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

theorem Hex.Matrix.rowReduce_rank_le_n {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.rank ≤ n

Wrapper-level projection of the rank row bound from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_rank_le_m {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.rank ≤ m

Wrapper-level projection of the rank column bound from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_pivotCols_sorted {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (i j : Fin M.rowReduce.rank) : i < j → M.rowReduce.pivotCols.get i < M.rowReduce.pivotCols.get j

Wrapper-level projection of pivot-column sortedness from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_transform_mul {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.transform * M = M.rowReduce.echelon

The transform returned by Hex.Matrix.rowReduce maps the input matrix to its echelon form.

theorem Hex.Matrix.rowReduce_isRowReduced {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.IsRowReduced M.rowReduce

The data computed by Hex.Matrix.rowReduce satisfies the Hex.Matrix.IsRowReduced contract.