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.det_row_multilinear: the determinant, as analternating_mapin the rows of the matrix
Main results #
det_mul: the determinant ofA ⬝ Bis 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.
def
matrix.det_row_multilinear
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
alternating_map R (n → R) R n
det is an alternating_map in the rows of the matrix.
def
matrix.det
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
R
The determinant of a matrix given by the Leibniz formula.
theorem
matrix.det_apply
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
M.det = ∑ (σ : equiv.perm n), ↑(⇑equiv.perm.sign σ) • ∏ (i : n), M (⇑σ i) i
theorem
matrix.det_apply'
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
M.det = ∑ (σ : equiv.perm n), (↑↑(⇑equiv.perm.sign σ)) * ∏ (i : n), M (⇑σ i) i
@[simp]
theorem
matrix.det_diagonal
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{d : n → R} :
(matrix.diagonal d).det = ∏ (i : n), d i
@[simp]
theorem
matrix.det_zero
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(h : nonempty n) :
@[simp]
theorem
matrix.det_eq_one_of_card_eq_zero
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(h : fintype.card n = 0) :
@[simp]
theorem
matrix.det_unique
{R : Type v}
[comm_ring R]
{n : Type u_1}
[unique n]
[decidable_eq n]
[fintype n]
(A : matrix n n R) :
If n has only one element, the determinant of an n by n matrix is just that element.
Although unique implies decidable_eq and fintype, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly.
theorem
matrix.det_eq_elem_of_card_eq_one
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(h : fintype.card n = 1)
(k : n) :
theorem
matrix.det_mul_aux
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{M N : matrix n n R}
{p : n → n}
(H : ¬function.bijective p) :
∑ (σ : equiv.perm n), (↑↑(⇑equiv.perm.sign σ)) * ∏ (x : n), (M (⇑σ x) (p x)) * N (p x) x = 0
@[instance]
def
matrix.det.is_monoid_hom
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
@[simp]
theorem
matrix.det_transpose
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
Transposing a matrix preserves the determinant.
theorem
matrix.det_permute
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(σ : equiv.perm n)
(M : matrix n n R) :
matrix.det (λ (i : n), M (⇑σ i)) = (↑(⇑equiv.perm.sign σ)) * M.det
Permuting the columns changes the sign of the determinant.
@[simp]
theorem
matrix.det_minor_equiv_self
{m : Type u_1}
{n : Type u_2}
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(e : n ≃ m)
(A : matrix m m R) :
Permuting rows and columns with the same equivalence has no effect.
theorem
matrix.det_reindex_self
{m : Type u_1}
{n : Type u_2}
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(e : m ≃ n)
(A : matrix m m R) :
(⇑(matrix.reindex e e) A).det = A.det
Reindexing both indices along the same equivalence preserves the determinant.
For the simp version of this lemma, see det_minor_equiv_self; this one is unsuitable because
matrix.reindex_apply unfolds reindex first.
@[simp]
theorem
matrix.det_permutation
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(σ : equiv.perm n) :
(equiv.to_pequiv σ).to_matrix.det = ↑(⇑equiv.perm.sign σ)
The determinant of a permutation matrix equals its sign.
@[simp]
theorem
matrix.det_smul
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
{c : R} :
theorem
matrix.ring_hom.map_det
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{S : Type w}
[comm_ring S]
{M : matrix n n R}
{f : R →+* S} :
det_zero section #
Prove that a matrix with a repeated column has determinant equal to zero.
theorem
matrix.det_eq_zero_of_row_eq_zero
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(i : n)
(h : ∀ (j : n), A i j = 0) :
theorem
matrix.det_eq_zero_of_column_eq_zero
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(j : n)
(h : ∀ (i : n), A i j = 0) :
theorem
matrix.det_zero_of_row_eq
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{M : matrix n n R}
{i j : n}
(i_ne_j : i ≠ j)
(hij : M i = M j) :
If a matrix has a repeated row, the determinant will be zero.
theorem
matrix.det_update_row_add
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R)
(j : n)
(u v : n → R) :
(M.update_row j (u + v)).det = (M.update_row j u).det + (M.update_row j v).det
theorem
matrix.det_update_column_add
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R)
(j : n)
(u v : n → R) :
(M.update_column j (u + v)).det = (M.update_column j u).det + (M.update_column j v).det
theorem
matrix.det_update_row_smul
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R)
(j : n)
(s : R)
(u : n → R) :
(M.update_row j (s • u)).det = s * (M.update_row j u).det
theorem
matrix.det_update_column_smul
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R)
(j : n)
(s : R)
(u : n → R) :
(M.update_column j (s • u)).det = s * (M.update_column j u).det
@[simp]
theorem
matrix.det_block_diagonal
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{o : Type u_1}
[fintype o]
[decidable_eq o]
(M : o → matrix n n R) :
(matrix.block_diagonal M).det = ∏ (k : o), (M k).det
theorem
matrix.upper_two_block_triangular_det
{m : Type u_1}
{n : Type u_2}
[decidable_eq n]
[fintype n]
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(A : matrix m m R)
(B : matrix m n R)
(D : matrix n n R) :
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
matrix.upper_block_triangular_det.