Block matrices and their determinant #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a predicate
matrix.block_triangular saying a matrix
is block triangular, and proves the value of the determinant for various
matrices built out of blocks.
Main definitions #
matrix.block_triangularexpresses that a
omatrix is block triangular, if the rows and columns are ordered according to some order
b : o → α
Main results #
matrix.det_of_block_triangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocks
matrix.det_of_lower_triangular: the determinant of a triangular matrix is the product of the entries along the diagonal
matrix, diagonal, det, block triangular
b map rows and columns of a square matrix
M to blocks indexed by
block_triangular M n b says the matrix is 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.
- hM.invertible_to_block k = (M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k)).invertible_of_left_inverse ((⅟ M).to_block (λ (i : m), b i < k) (λ (i : m), b i < k)) _
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.