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_triangular expresses that a
o matrix is block triangular,
if the rows and columns are ordered according to some order
b : o → α
Main results #
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.
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.