Block Matrices #
Main definitions #
Matrix.fromBlocks
: build a block matrix out of 4 blocksMatrix.toBlocks₁₁
,Matrix.toBlocks₁₂
,Matrix.toBlocks₂₁
,Matrix.toBlocks₂₂
: extract each of the four blocks fromMatrix.fromBlocks
.Matrix.blockDiagonal
: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,Matrix.blockDiagonalRingHom
.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.blockDiagonal'RingHom
.Matrix.blockDiag'
: extract the blocks from the diagonal of a block diagonal matrix.
Let p
pick out certain rows and columns of a square matrix M
. Then
toSquareBlockProp M p
is the corresponding block matrix.
Instances For
Let b
map rows and columns of a square matrix M
to blocks. Then
toSquareBlock M b k
is the block k
matrix.
Instances For
Matrix.blockDiagonal M
turns a homogenously-indexed collection of matrices
M : o → Matrix m n α'
into an m × o
-by-n × o
block matrix which has the entries of M
along
the diagonal and zero elsewhere.
See also Matrix.blockDiagonal'
if the matrices may not have the same size everywhere.
Instances For
Matrix.blockDiagonal
as an AddMonoidHom
.
Instances For
Matrix.blockDiagonal
as a RingHom
.
Instances For
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of Matrix.diag
, and the left-inverse of Matrix.blockDiagonal
.
Instances For
Matrix.blockDiag
as an AddMonoidHom
.
Instances For
Matrix.blockDiagonal' M
turns M : Π i, Matrix (m i) (n i) α
into a
Σ i, m i
-by-Σ i, n i
block matrix which has the entries of M
along the diagonal
and zero elsewhere.
This is the dependently-typed version of Matrix.blockDiagonal
.
Instances For
Matrix.blockDiagonal'
as an AddMonoidHom
.
Instances For
Matrix.blockDiagonal'
as a RingHom
.
Instances For
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of Matrix.diag
, and the left-inverse of Matrix.blockDiagonal'
.
Instances For
Matrix.blockDiag'
as an AddMonoidHom
.