hex

12.3. Gauss-Jordan reduction🔗

The driver is Gauss-Jordan elimination. It returns a Hex.Matrix.RowEchelonData satisfying Hex.Matrix.IsRowReduced, with the transform equation and the rank read off the result.

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

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

🔗theorem
Hex.Matrix.rowReduce_transform_mul.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m) :
  M.rowReduce.transform * M = M.rowReduce.echelon
Hex.Matrix.rowReduce_transform_mul.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.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.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m) :
  M.IsRowReduced M.rowReduce
Hex.Matrix.rowReduce_isRowReduced.{u}
  {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R]
  (M : Hex.Matrix R n m) :
  M.IsRowReduced M.rowReduce

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

🔗def
Hex.Matrix.rowReduce_rank.{u} {R : Type u} {n m : ℕ}
  [Lean.Grind.Field R] [DecidableEq R] (M : Hex.Matrix R n m) : ℕ
Hex.Matrix.rowReduce_rank.{u} {R : Type u}
  {n m : ℕ} [Lean.Grind.Field R]
  [DecidableEq R] (M : Hex.Matrix R n m) :
  ℕ

The rank returned by Hex.Matrix.rowReduce.