hex

23.3. Entry points🔗

The generic public entry points Hex.Matrix.bareissDataWith and Hex.Matrix.bareissWith run the row-pivoting elimination with an explicit quotient operation. The traditional integer entry points specialize them to the native exact quotient. Hex.Matrix.bareissData returns the full record. Hex.Matrix.bareiss returns just the integer determinant. The no-pivot variants skip the pivot search, for inputs whose leading pivots are already nonzero.

🔗def
Hex.Matrix.bareissDataWith.{u} {R : Type u} {n : ℕ} [Zero R] [One R]
  [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R)
  (M : Hex.Matrix R n n) : Hex.Matrix.BareissData R n
Hex.Matrix.bareissDataWith.{u}
  {R : Type u} {n : ℕ} [Zero R] [One R]
  [Sub R] [Mul R] [DecidableEq R]
  (quot : R → R → R)
  (M : Hex.Matrix R n n) :
  Hex.Matrix.BareissData R n

Run the row-pivoted Bareiss elimination and return the final elimination data together with the swap/sign bookkeeping.

🔗def
Hex.Matrix.bareissWith.{u} {R : Type u} {n : ℕ} [Zero R] [One R] [Neg R]
  [Sub R] [Mul R] [DecidableEq R] (quot : R → R → R)
  (M : Hex.Matrix R n n) : R
Hex.Matrix.bareissWith.{u} {R : Type u}
  {n : ℕ} [Zero R] [One R] [Neg R] [Sub R]
  [Mul R] [DecidableEq R]
  (quot : R → R → R)
  (M : Hex.Matrix R n n) : R

Determinant computed by the row-pivoted Bareiss algorithm.

🔗def
Hex.Matrix.bareissData {n : ℕ} (M : Hex.Matrix ℤ n n) :
  Hex.Matrix.BareissData ℤ n
Hex.Matrix.bareissData {n : ℕ}
  (M : Hex.Matrix ℤ n n) :
  Hex.Matrix.BareissData ℤ n

Integer specialization returning row-pivoted elimination data.

🔗def
Hex.Matrix.bareiss {n : ℕ} (M : Hex.Matrix ℤ n n) : ℤ
Hex.Matrix.bareiss {n : ℕ}
  (M : Hex.Matrix ℤ n n) : ℤ

Integer specialization of the row-pivoted Bareiss determinant.

🔗def
Hex.Matrix.bareissNoPivotData {n : ℕ} (M : Hex.Matrix ℤ n n) :
  Hex.Matrix.BareissData ℤ n
Hex.Matrix.bareissNoPivotData {n : ℕ}
  (M : Hex.Matrix ℤ n n) :
  Hex.Matrix.BareissData ℤ n

Integer specialization returning no-pivot elimination data.

🔗def
Hex.Matrix.bareissNoPivot {n : ℕ} (M : Hex.Matrix ℤ n n) : ℤ
Hex.Matrix.bareissNoPivot {n : ℕ}
  (M : Hex.Matrix ℤ n n) : ℤ

Integer specialization of the no-pivot Bareiss determinant.

For integers, the quotient specializes to the GMP-backed lean_int_div_exact primitive. The executable loop does not carry a divisibility proof; the Mathlib correspondence proves exactness from the quotient cancellation law. The bordered minors are the intermediate determinants used as the elimination invariant.

🔗def
Hex.Matrix.borderedMinor.{u_1} {R : Type u_1} {n : ℕ}
  (M : Hex.Matrix R n n) (k : ℕ) (hk : k < n) (i j : Fin n) :
  Hex.Matrix R (k + 1) (k + 1)
Hex.Matrix.borderedMinor.{u_1}
  {R : Type u_1} {n : ℕ}
  (M : Hex.Matrix R n n) (k : ℕ)
  (hk : k < n) (i j : Fin n) :
  Hex.Matrix R (k + 1) (k + 1)

Bordered Bareiss minor with the first k rows/columns and one extra border row i and column j. For Bareiss applications i and j are in the trailing part, but the constructor is total and leaves that side condition to the invariant using it.