hex

23.2. The elimination record🔗

An elimination pass returns a small record: the terminal matrix, the number of row swaps performed during pivoting, and an optional record of the first step at which a zero pivot with no replacement row was found (the signal that the matrix is singular).

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

Output of an executable Bareiss elimination pass.

Constructor

Hex.Matrix.BareissData.mk.{u}

Fields

matrix : Hex.Matrix R n n

Terminal matrix produced by the Bareiss pass. When singularStep = none, BareissData.det reads the last diagonal entry of this matrix, with the row-swap sign applied; for n = 0, the empty diagonal contributes 1.

rowSwaps : ℕ

Number of row swaps performed by pivoting. Even parity contributes sign 1; odd parity contributes sign -1.

singularStep : Option ℕ

The first elimination step that found a zero pivot and no replacement row. A value some k records that singular step and makes BareissData.det return 0; none means the run reached the terminal diagonal encoding.

The sign contributed by the row swaps and the encoded determinant are read off that record. A recorded singular step encodes determinant zero. Otherwise the determinant is the last diagonal entry of the terminal matrix with the swap sign applied.

🔗def
Hex.Matrix.BareissData.sign.{u} {R : Type u} {n : ℕ} [One R] [Neg R]
  (data : Hex.Matrix.BareissData R n) : R
Hex.Matrix.BareissData.sign.{u}
  {R : Type u} {n : ℕ} [One R] [Neg R]
  (data : Hex.Matrix.BareissData R n) : R

The determinant sign contributed by the recorded row swaps.

🔗def
Hex.Matrix.BareissData.det.{u} {R : Type u} {n : ℕ} [Zero R] [One R]
  [Neg R] [Mul R] (data : Hex.Matrix.BareissData R n) : R
Hex.Matrix.BareissData.det.{u}
  {R : Type u} {n : ℕ} [Zero R] [One R]
  [Neg R] [Mul R]
  (data : Hex.Matrix.BareissData R n) : R

The determinant encoded by a Bareiss elimination result.