Commit 2022-10-13 08:46 46fc73a3

View on Github →

feat(linear_algebra/matrix): inverse of block triangular is block triangular (#16150) The inverse of a block triangular matrix is block triangular. I took the opportunity to refactor the proof about determinants of block triangular matrices as well.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem image_subtype_ne_univ_eq_image_erase

added theorem image_subtype_univ_ssubset_image_univ

Modified src/data/matrix/block.lean

modified theorem matrix.from_blocks_diagonal

modified theorem matrix.from_blocks_one

added theorem matrix.to_block_diagonal_disjoint

added theorem matrix.to_block_diagonal_self

added theorem matrix.to_block_mul_eq_add

added theorem matrix.to_block_mul_eq_mul

added theorem matrix.to_block_one_disjoint

added theorem matrix.to_block_one_self

Modified src/linear_algebra/matrix/block.lean

added theorem matrix.block_triangular.add

added theorem matrix.block_triangular.inv_to_block

added def matrix.block_triangular.invertible_to_block

added theorem matrix.block_triangular.mul

added theorem matrix.block_triangular.sub

added theorem matrix.block_triangular.to_block_inverse_mul_to_block_eq_one

added theorem matrix.block_triangular_block_diagonal'

added theorem matrix.block_triangular_block_diagonal

added theorem matrix.block_triangular_diagonal

added theorem matrix.block_triangular_inv_of_block_triangular

added theorem matrix.block_triangular_zero

added theorem matrix.to_block_inverse_eq_zero