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 permutationsMatrix.detRowAlternating
: the determinant, as anAlternatingMap
in the rows of the matrix
Main results #
det_mul
: the determinant ofA * B
is the product of determinantsdet_zero_of_row_eq
: the determinant is zero if there is a repeated rowdet_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 AlternatingMap
in the rows of the matrix.
Equations
- Matrix.detRowAlternating = MultilinearMap.alternatization (MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebra R n R) LinearMap.proj)
Instances For
The determinant of a matrix given by the Leibniz formula.
Equations
- Matrix.det M = Matrix.detRowAlternating M
Instances For
If n
has only one element, the determinant of an n
by n
matrix is just that element.
Although Unique
implies DecidableEq
and Fintype
, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly.
The determinant of a matrix, as a monoid homomorphism.
Equations
- Matrix.detMonoidHom = { toOneHom := { toFun := Matrix.det, map_one' := ⋯ }, map_mul' := ⋯ }
Instances For
On square matrices, mul_left_comm
applies under det
.
On square matrices, mul_right_comm
applies under det
.
Transposing a matrix preserves the determinant.
Permuting the columns changes the sign of the determinant.
Permuting rows and columns with the same equivalence has no effect.
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_submatrix_equiv_self
; this one is unsuitable because
Matrix.reindex_apply
unfolds reindex
first.
The determinant of a permutation matrix equals its sign.
A variant of Matrix.det_neg
with scalar multiplication by Units ℤ
instead of multiplication
by R
.
Multiplying each row by a fixed v i
multiplies the determinant by
the product of the v
s.
Multiplying each column by a fixed v j
multiplies the determinant by
the product of the v
s.
If a matrix has a repeated row, the determinant will be zero.
If a matrix has a repeated column, the determinant will be zero.
det_eq
section #
Lemmas showing the determinant is invariant under a variety of operations.
If you add multiples of row B k
to other rows, the determinant doesn't change.
If you add multiples of previous rows to the next row, the determinant doesn't change.
If you add multiples of previous columns to the next columns, the determinant doesn't change.
The determinant of a 2×2 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
Matrix.det_of_upper_triangular
.
The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of
the determinants of the diagonal blocks. For the generalization to any number of blocks, see
Matrix.det_of_lower_triangular
.
Laplacian expansion of the determinant of an n+1 × n+1
matrix along column 0.
Laplacian expansion of the determinant of an n+1 × n+1
matrix along row 0.
Laplacian expansion of the determinant of an n+1 × n+1
matrix along row i
.
Laplacian expansion of the determinant of an n+1 × n+1
matrix along column j
.
Determinant of 0x0 matrix
Determinant of 1x1 matrix