theorem Hex.Matrix.detSign_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (v : Vector (Fin n) n) : detSign (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = detSign v

Appending the new largest value in the last position does not change the determinant sign, because it adds no inversions.

theorem Hex.Matrix.detSign_identity {R : Type u} [Lean.Grind.Ring R] (n : Nat) : detSign (Vector.ofFn fun (i : Fin n) => i) = 1

The identity permutation has positive determinant sign.

theorem Hex.Matrix.detProduct_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (v : Vector (Fin n) n) : M.detProduct (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = (M.principalSubmatrix n ⋯).detProduct v * M[Fin.last n][Fin.last n]

Product reindexing for a permutation that fixes the final column. The Leibniz product splits into the product on the leading prefix times the final row/column entry.

theorem Hex.Matrix.detTerm_insertAt_last {R : Type u} [Lean.Grind.Ring R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (v : Vector (Fin n) n) : M.detTerm (insertAt (Fin.last n) (Vector.map Fin.castSucc v) (Fin.last n)) = detSign v * ((M.principalSubmatrix n ⋯).detProduct v * M[Fin.last n][Fin.last n])

Leibniz-term reindexing for a permutation that fixes the final column. This packages the sign and product split used by last-row/last-column expansions.

theorem Hex.Matrix.det_eq_principalSubmatrix_mul_last {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R (n + 1) (n + 1)) (hrow : ∀ (j : Fin (n + 1)), ↑j < n → M[Fin.last n][j] = 0) : M.det = (M.principalSubmatrix n ⋯).det * M[Fin.last n][Fin.last n]

If the last row is zero before the diagonal entry, the determinant factors as the leading principal determinant times the bottom-right entry. This is the triangular-recursion step used by positivity and diagonal-product lemmas.