Determinant of a matrix #
This file defines the determinant of a matrix,
matrix.det, and its essential properties.
Main definitions #
matrix.det: the determinant of a square matrix, as a sum over permutations
matrix.det_row_multilinear: the determinant, as an
alternating_mapin the rows of the matrix
Main results #
det_mul: the determinant of
A ⬝ Bis the product of determinants
det_zero_of_row_eq: the determinant is zero if there is a repeated row
det_block_diagonal: the determinant of a block diagonal matrix is a product of the blocks' determinants
Implementation notes #
It is possible to configure
simp to compute determinants. See the file
test/matrix.lean for some examples.
det is an
alternating_map in the rows of the matrix.
n has only one element, the determinant of an
n matrix is just that element.
fintype, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly.
Reindexing both indices along the same equivalence preserves the determinant.
simp version of this lemma, see
det_minor_equiv_self; this one is unsuitable because
det_zero section #
Prove that a matrix with a repeated column has determinant equal to zero.
The determinant of a 2x2 block matrix with the lower-left block equal to zero is the product of
the determinants of the diagonal blocks. For the generalization to any number of blocks, see