Determinant of triangular matrices.

The determinant of an upper- or lower-triangular square matrix is the product of its diagonal entries. The upper-triangular case recurses on the last row via the factorisation in HexDeterminant.LastRow; the lower-triangular case is derived from it through det_transpose.

theorem Hex.Matrix.det_upperTriangular_pos_diag {n : Nat} (M : Matrix Int n n) (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) (hdiag : ∀ (i : Fin n), 0 < M[i][i]) : 0 < M.det

An integer upper-triangular matrix with strictly positive diagonal has strictly positive determinant.

theorem Hex.Matrix.det_upperTriangular_eq_finFoldl_diag {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) : M.det = Fin.foldl n (fun (acc : R) (i : Fin n) => acc * M[i][i]) 1

The determinant of an upper-triangular square matrix (entries below the diagonal are zero) over a commutative ring is the product of its diagonal entries, expressed via a Fin.foldl over the diagonal indices.

theorem Hex.Matrix.det_upperTriangular_eq_foldl_diag {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) : M.det = List.foldl (fun (acc : R) (i : Fin n) => acc * M[i][i]) 1 (List.finRange n)

The determinant of an upper-triangular square matrix as a List.foldl product over the diagonal indices in Fin.finRange.

theorem Hex.Matrix.det_lowerTriangular_eq_finFoldl_diag {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (hzero : ∀ (i j : Fin n), ↑i < ↑j → M[i][j] = 0) : M.det = Fin.foldl n (fun (acc : R) (i : Fin n) => acc * M[i][i]) 1

Diagonal-product formula for the determinant of a lower-triangular matrix (entries above the diagonal are zero). Derived from the upper-triangular form via det_transpose.

theorem Hex.Matrix.det_lowerTriangular_eq_foldl_diag {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (M : Matrix R n n) (hzero : ∀ (i j : Fin n), ↑i < ↑j → M[i][j] = 0) : M.det = List.foldl (fun (acc : R) (i : Fin n) => acc * M[i][i]) 1 (List.finRange n)

The determinant of a lower-triangular square matrix as a List.foldl product over the diagonal indices in Fin.finRange.