mathlib documentation

linear_algebra.determinant

Determinant of a matrix #

This file defines the determinant of a matrix, matrix.det, and its essential properties.

Main definitions #

Main results #

Implementation notes #

It is possible to configure simp to compute determinants. See the file test/matrix.lean for some examples.

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) :
0.det = 0
@[simp]
theorem matrix.det_one {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
1.det = 1
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) :
A.det = 1
@[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) :
A.det = A (default n) (default n)

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) :
A.det = A k k
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
@[simp]
theorem matrix.det_mul {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (M N : matrix n n R) :
(M N).det = (M.det) * N.det
@[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) :
(A.minor e e).det = A.det

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) :

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) :

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} :
(c A).det = (c ^ fintype.card n) * A.det
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} :
theorem matrix.alg_hom.map_det {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {S : Type w} [comm_ring S] [algebra R S] {T : Type z} [comm_ring T] [algebra R T] {M : matrix n n S} {f : S →ₐ[R] T} :

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) :
A.det = 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) :
A.det = 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) :
M.det = 0

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) :
(A.from_blocks B 0 D).det = (A.det) * D.det

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.