Block matrices and their determinant #
This file defines a predicate
Matrix.BlockTriangular saying a matrix
is block triangular, and proves the value of the determinant for various
matrices built out of blocks.
Main definitions #
Matrix.BlockTriangularexpresses that an
omatrix is block triangular, if the rows and columns are ordered according to some order
b : o → α
Main results #
Matrix.det_of_blockTriangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocks
matrix.det_of_lowerTriangular: the determinant of a triangular matrix is the product of the entries along the diagonal
matrix, diagonal, det, block triangular
The inverse of an upper-left subblock of a block-triangular matrix
M is the upper-left
An upper-left subblock of an invertible block-triangular matrix is invertible.
A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step
The inverse of a block-triangular matrix is block-triangular.