structure Hex.Matrix.RowReduceState (R : Type u) (n m : Nat) : Type u

• row : Nat
• echelon : Matrix R n m
• transform : Matrix R n n
• pivots : List (Fin m)

def Hex.Matrix.rowReduceLoop {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (col fuel : Nat) (state : RowReduceState R n m) : RowReduceState R n m

Process columns left-to-right, performing Gauss-Jordan elimination.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.rowReduceLoop col 0 state = state