Block Matrices #
Main definitions #
Matrix.fromBlocks: build a block matrix out of 4 blocks
Matrix.toBlocks₂₂: extract each of the four blocks from
Matrix.blockDiagonal: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,
Matrix.blockDiag: extract the blocks from the diagonal of a block diagonal matrix.
Matrix.blockDiagonal': block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms,
Matrix.blockDiag': extract the blocks from the diagonal of a block diagonal matrix.
We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.
Two block matrices are equal if their blocks are equal.
Matrix.blockDiagonal' if the matrices may not have the same size everywhere.
This is the dependently-typed version of
Extract a block from the diagonal of a block diagonal matrix.