theorem HexMatrixMathlib.ordered_four_det_mul_det_setRow_setRow_eq_cofactorRowPairing_mul_sub {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; have r3 := ⟨↑p3 - 1, ⋯⟩; M.det * ((M.setRow r2 B[p1]).setRow r3 B[q]).det = M.cofactorRowPairing r2 B[p1] * M.cofactorRowPairing r3 B[q] - M.cofactorRowPairing r3 B[p1] * M.cofactorRowPairing r2 B[q]

theorem HexMatrixMathlib.ordered_four_det_nMatrix_eq_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have hp1q := ⋯; (B.nMatrix p1 q hp1q).det = B.nDet p1 q hp1q

The ordered base minor in the four-row Plucker setup is exactly the corresponding nDet. This theorem gives downstream rewrites a named surface instead of unfolding Hex.Matrix.nDet locally.

theorem HexMatrixMathlib.ordered_four_det_mul_det_setRow_setRow_eq_det_setRow_mul_sub {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have M := B.nMatrix p1 q ⋯; have r2 := ⟨↑p2 - 1, ⋯⟩; have r3 := ⟨↑p3 - 1, ⋯⟩; M.det * ((M.setRow r2 B[p1]).setRow r3 B[q]).det = (M.setRow r2 B[p1]).det * (M.setRow r3 B[q]).det - (M.setRow r3 B[p1]).det * (M.setRow r2 B[q]).det

Ordered two-row replacement identity after rewriting each cofactor-row pairing as the determinant of the corresponding row replacement.

This is the determinant-only form needed before the remaining signed row-permutation transports to nDet minors.

theorem HexMatrixMathlib.det_double_setRow_eq_pow_mul_nDet {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have h1q := ⋯; have M := B.nMatrix p1 q h1q; have r2 := ⟨↑p2 - 1, ⋯⟩; have r3 := ⟨↑p3 - 1, ⋯⟩; ((M.setRow r2 B[p1]).setRow r3 B[q]).det = (-1) ^ (↑p2 - ↑p1 - 1 + (↑q - ↑p3 - 1)) * B.nDet p2 p3 h23

Determinant-level transport for the ordered four-row double setRow: for p1 < p2 < p3 < q, replacing rows r2 := ⟨p2.val - 1, _⟩ and r3 := ⟨p3.val - 1, _⟩ of nMatrix B p1 q by B[p1] and B[q] respectively produces the signed nDet B p2 p3 minor with combined sign (-1) ^ (p2.val - p1.val - 1 + (q.val - p3.val - 1)).

theorem HexMatrixMathlib.ordered_four_signed_Plucker_p1_side {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : have h1q := ⋯; have h2q := ⋯; have M := B.nMatrix p1 q h1q; have r2 := ⟨↑p2 - 1, ⋯⟩; have r3 := ⟨↑p3 - 1, ⋯⟩; B.nDet p1 q h1q * ((-1) ^ (↑p2 - ↑p1 - 1 + (↑q - ↑p3 - 1)) * B.nDet p2 p3 h23) = (-1) ^ (↑p2 - ↑p1 - 1) * B.nDet p2 q h2q * M.cofactorRowPairing r3 B[q] - (-1) ^ (↑p3 - ↑p1 - 1) * B.nDet p3 q h3q * M.cofactorRowPairing r2 B[q]

Rewrite-ready signed Plucker form: the LHS double-row setRow determinant is identified with the signed nDet B p2 p3 minor, and the two p1-side cofactor-row pairings on the RHS are identified with their signed nDet B p_t q minors. The remaining q-side cofactor-row pairings are left in cofactorRowPairing form so the assembly in can finish them after the q-row signed transports land.

theorem HexMatrixMathlib.det_plucker_three_term_nDet_of_ordered_four {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (h3q : ↑p3 < ↑q) : B.nDet p2 p3 h23 * B.nDet p1 q ⋯ - B.nDet p1 p3 ⋯ * B.nDet p2 q ⋯ + B.nDet p1 p2 h12 * B.nDet p3 q h3q = 0

Raw ordered four-row nDet Plucker kernel. For p1 < p2 < p3 < q, the canonical three-term Grassmann-Plucker identity holds among the six ordered nDet minors of B. The proof substitutes the q-side cofactor-row pairings in ordered_four_signed_Plucker_p1_side to obtain a fully-signed nDet identity, then cancels the common (-1) ^ (p2.val - p1.val - 1 + (q.val - p3.val - 1)) factor by squaring it.

theorem HexMatrixMathlib.det_plucker_three_term_basisVec_of_ne {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (p1 p2 p3 q : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) (hq1 : q ≠ p1) (hq2 : q ≠ p2) (hq3 : q ≠ p3) : B.mDet (Vector.unit R q) p1 * B.nDet p2 p3 h23 - B.mDet (Vector.unit R q) p2 * B.nDet p1 p3 ⋯ + B.mDet (Vector.unit R q) p3 * B.nDet p1 p2 h12 = 0

Arbitrary-row basis-vector Plucker coefficient identity for three ordered rows p1 < p2 < p3 and a fourth row q distinct from them. The proof transports each order case to the ordered four-row nDet kernel and rewrites the three mDet coefficients by basis-vector evaluation.

theorem HexMatrixMathlib.det_plucker_three_term {R : Type u} [CommRing R] {n : ℕ} (B : Hex.Matrix R (n + 3) (n + 1)) (v : Vector R (n + 3)) (p1 p2 p3 : Fin (n + 3)) (h12 : ↑p1 < ↑p2) (h23 : ↑p2 < ↑p3) : B.mDet v p1 * B.nDet p2 p3 h23 - B.mDet v p2 * B.nDet p1 p3 ⋯ + B.mDet v p3 * B.nDet p1 p2 h12 = 0

Universal three-term Plucker identity for one arbitrary row and three ordered basis rows, assembled from the ordered four-row nDet kernel and the three equal-row basis-vector cases.

def HexMatrixMathlib.bareissDesnanotIndex (k : ℕ) : Fin (k + 2) ≃ Fin (k + 2)

Reindex the (k+2) × (k+2) bordered minor so Desnanot-Jacobi deletes the Bareiss pivot row/column first and the trailing row/column last.

The order is [k, 0, 1, ..., k-1, k+1] in the original bordered-minor coordinates. Applying the same permutation to rows and columns preserves the determinant and makes the Desnanot interior the previous leading pivot.

Equations

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

@[simp]

theorem HexMatrixMathlib.bareissDesnanotIndex_zero (k : ℕ) : (bareissDesnanotIndex k) 0 = ⟨k, ⋯⟩

@[simp]

theorem HexMatrixMathlib.bareissDesnanotIndex_last (k : ℕ) : (bareissDesnanotIndex k) (Fin.last (k + 1)) = Fin.last (k + 1)

theorem HexMatrixMathlib.det_borderedMinor_bareissDesnanotIndex {R : Type u} {n : ℕ} [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hnext : k + 1 < n) (i j : Fin n) : ((matrixEquiv (source.borderedMinor (k + 1) hnext i j)).submatrix ⇑(bareissDesnanotIndex k) ⇑(bareissDesnanotIndex k)).det = (source.borderedMinor (k + 1) hnext i j).det

Reindexing a bordered minor by bareissDesnanotIndex on both axes does not change its determinant.

theorem HexMatrixMathlib.desnanot_jacobi_borderedMinor_reindex {R : Type u} {n : ℕ} [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hnext : k + 1 < n) (i j : Fin n) : have M := (matrixEquiv (source.borderedMinor (k + 1) hnext i j)).submatrix ⇑(bareissDesnanotIndex k) ⇑(bareissDesnanotIndex k); M.det * (M.submatrix (Fin.succAbove 0 ∘ (Fin.last k).succAbove) (Fin.succAbove 0 ∘ (Fin.last k).succAbove)).det = (M.submatrix (Fin.succAbove 0) (Fin.succAbove 0)).det * (M.submatrix (Fin.last (k + 1)).succAbove (Fin.last (k + 1)).succAbove).det - (M.submatrix (Fin.succAbove 0) (Fin.last (k + 1)).succAbove).det * (M.submatrix (Fin.last (k + 1)).succAbove (Fin.succAbove 0)).det

Desnanot-Jacobi specialized to a Bareiss bordered minor after the row/column reindexing used by bareissDesnanotIndex.

This is the Mathlib determinant identity that later proofs rewrite through matrixEquiv_borderedMinor/det_borderedMinor_eq_submatrix_det to obtain the hdesnanot hypothesis for bareissExactDiv_borderedMinor_of_mul_eq.

theorem HexMatrixMathlib.bareissExactDiv_borderedMinor_of_mul_eq {n : ℕ} (source : Hex.Matrix ℤ n n) (k : ℕ) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) (prevPivot : ℤ) (hprev_ne : prevPivot ≠ 0) (hdesnanot : (source.borderedMinor (k + 1) hnext i j).det * prevPivot = (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) : Hex.Matrix.exactDiv ((source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det) prevPivot = (source.borderedMinor (k + 1) hnext i j).det

Exact-division equation for one Bareiss bordered-minor update.

The remaining Mathlib-side recurrence proof can supply hdesnanot from the Desnanot-Jacobi identity; this lemma packages the resulting product identity as the hexact premise expected by Hex.Matrix.stepMatrix_borderedMinor_update.

theorem HexMatrixMathlib.desnanot_jacobi_borderedMinor {R : Type u} {n : ℕ} [CommRing R] (source : Hex.Matrix R n n) (k : ℕ) (hk : k < n) (hnext : k + 1 < n) (i j : Fin n) (hi : k < ↑i) (hj : k < ↑j) : (source.borderedMinor (k + 1) hnext i j).det * (source.principalSubmatrix k ⋯).det = (source.borderedMinor k hk ⟨k, ⋯⟩ ⟨k, ⋯⟩).det * (source.borderedMinor k hk i j).det - (source.borderedMinor k hk i ⟨k, ⋯⟩).det * (source.borderedMinor k hk ⟨k, ⋯⟩ j).det

Desnanot-Jacobi specialised to a Bareiss bordered minor: the Mathlib determinant identity from desnanot_jacobi_borderedMinor_reindex translated back into Hex borderedMinor/principalSubmatrix determinants. This produces the hdesnanot premise expected by bareissExactDiv_borderedMinor_of_mul_eq with prevPivot instantiated as det (principalSubmatrix source k _).