Determinants of dependent block-diagonal matrices #
The determinant of a block-diagonal matrix Matrix.blockDiagonal' M whose blocks may have
different index types is the product of the determinants of its blocks. This is the dependent
version of Mathlib's Matrix.det_blockDiagonal, and computes the determinant of a coordinatewise
endomorphism of a finite dependent product.
Main results #
Matrix.det_blockDiagonal':(blockDiagonal' M).det = ∏ i, (M i).det.
@[simp]
theorem
Matrix.det_blockDiagonal'
{o : Type u_1}
{R : Type u_2}
{m : o → Type u_3}
[Fintype o]
[DecidableEq o]
[(i : o) → Fintype (m i)]
[(i : o) → DecidableEq (m i)]
[CommRing R]
(M : (i : o) → Matrix (m i) (m i) R)
:
The determinant of a block-diagonal matrix with blocks of possibly different sizes is the
product of the determinants of the blocks. This is the dependent version of
Matrix.det_blockDiagonal.