Commit 2023-04-27 06:19 55d59ba1

View on Github →

feat: port LinearAlgebra.Matrix.Block (#3667)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Block.lean

added theorem Matrix.BlockTriangular.add

added theorem Matrix.BlockTriangular.det_fintype

added theorem Matrix.BlockTriangular.inv_toBlock

added def Matrix.BlockTriangular.invertibleToBlock

added theorem Matrix.BlockTriangular.mul

added theorem Matrix.BlockTriangular.sub

added theorem Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one

added def Matrix.BlockTriangular

added theorem Matrix.blockTriangular_blockDiagonal'

added theorem Matrix.blockTriangular_blockDiagonal

added theorem Matrix.blockTriangular_diagonal

added theorem Matrix.blockTriangular_inv_of_blockTriangular

added theorem Matrix.blockTriangular_reindex_iff

added theorem Matrix.blockTriangular_zero

added theorem Matrix.det_of_lowerTriangular

added theorem Matrix.det_of_upperTriangular

added theorem Matrix.det_toBlock

added theorem Matrix.det_toSquareBlock_id

added theorem Matrix.equiv_block_det

added theorem Matrix.toBlock_inverse_eq_zero

added theorem Matrix.twoBlockTriangular_det'

added theorem Matrix.twoBlockTriangular_det

added theorem Matrix.upper_two_blockTriangular