mathlib3 documentation

linear_algebra.matrix.determinant

Determinant of a matrix #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
def matrix.det_row_alternating {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.

Equations
source
@[reducible]
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.

source
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 = finset.univ.sum (λ (σ : equiv.perm n), ⇑equiv.perm.sign σ • finset.univ.prod (λ (i : n), M (⇑σ i) i))
source
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 = finset.univ.sum (λ (σ : equiv.perm n), ↑↑(⇑equiv.perm.sign σ) * finset.univ.prod (λ (i : n), M (⇑σ i) i))
source
@[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 = finset.univ.prod (λ (i : n), d i)
source
@[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
source
@[simp]
theorem matrix.det_one {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
1.det = 1
source
theorem matrix.det_is_empty {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [is_empty n] {A : matrix n n R} :
A.det = 1
source
@[simp]
theorem matrix.coe_det_is_empty {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [is_empty n] :
matrix.det = function.const (matrix n n R) 1
source
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
source
@[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 inhabited.default inhabited.default

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.

source
theorem matrix.det_eq_elem_of_subsingleton {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [subsingleton n] (A : matrix n n R) (k : n) :
A.det = A k k
source
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
source
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) :
finset.univ.sum (λ (σ : equiv.perm n), ↑↑(⇑equiv.perm.sign σ) * finset.univ.prod (λ (x : n), M (⇑σ x) (p x) * N (p x) x)) = 0
source
@[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.mul N).det = M.det * N.det
source
def matrix.det_monoid_hom {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
matrix n n R →* R

The determinant of a matrix, as a monoid homomorphism.

Equations
source
@[simp]
theorem matrix.coe_det_monoid_hom {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
⇑matrix.det_monoid_hom = matrix.det
source
theorem matrix.det_mul_comm {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M N : matrix m m R) :
(M.mul N).det = (N.mul M).det

On square matrices, mul_comm applies under det.

source
theorem matrix.det_mul_left_comm {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M N P : matrix m m R) :
(M.mul (N.mul P)).det = (N.mul (M.mul P)).det

On square matrices, mul_left_comm applies under det.

source
theorem matrix.det_mul_right_comm {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M N P : matrix m m R) :
((M.mul N).mul P).det = ((M.mul P).mul N).det

On square matrices, mul_right_comm applies under det.

source
theorem matrix.det_units_conj {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : (matrix m m R)ˣ) (N : matrix m m R) :
((↑M.mul N).mul ↑M⁻¹).det = N.det
source
theorem matrix.det_units_conj' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : (matrix m m R)ˣ) (N : matrix m m R) :
((↑M⁻¹.mul N).mul ↑M).det = N.det
source
@[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) :
M.transpose.det = M.det

Transposing a matrix preserves the determinant.

source
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.

source
@[simp]
theorem matrix.det_submatrix_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.submatrix ⇑e ⇑e).det = A.det

Permuting rows and columns with the same equivalence has no effect.

source
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_submatrix_equiv_self; this one is unsuitable because matrix.reindex_apply unfolds reindex first.

source
@[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.

source
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
source
@[simp]
theorem matrix.det_smul_of_tower {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {α : Type u_1} [monoid α] [distrib_mul_action α R] [is_scalar_tower α R R] [smul_comm_class α R R] (c : α) (A : matrix n n R) :
(c • A).det = c ^ fintype.card n • A.det
source
theorem matrix.det_neg {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) :
(-A).det = (-1) ^ fintype.card n * A.det
source
theorem matrix.det_neg_eq_smul {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) :
(-A).det = (-1) ^ fintype.card n • A.det

A variant of matrix.det_neg with scalar multiplication by units ℤ instead of multiplication by R.

source
theorem matrix.det_mul_row {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (v : n → R) (A : matrix n n R) :
(⇑matrix.of (λ (i j : n), v j * A i j)).det = finset.univ.prod (λ (i : n), v i) * A.det

Multiplying each row by a fixed v i multiplies the determinant by the product of the vs.

source
theorem matrix.det_mul_column {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (v : n → R) (A : matrix n n R) :
(⇑matrix.of (λ (i j : n), v i * A i j)).det = finset.univ.prod (λ (i : n), v i) * A.det

Multiplying each column by a fixed v j multiplies the determinant by the product of the vs.

source
@[simp]
theorem matrix.det_pow {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (n : ℕ) :
(M ^ n).det = M.det ^ n
source
theorem 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] (f : R →+* S) (M : matrix n n R) :
⇑f M.det = (⇑(f.map_matrix) M).det
source
theorem ring_equiv.map_det {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {S : Type w} [comm_ring S] (f : R ≃+* S) (M : matrix n n R) :
⇑f M.det = (⇑(f.map_matrix) M).det
source
theorem 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] (f : S →ₐ[R] T) (M : matrix n n S) :
⇑f M.det = (⇑(f.map_matrix) M).det
source
theorem alg_equiv.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] (f : S ≃ₐ[R] T) (M : matrix n n S) :
⇑f M.det = (⇑(f.map_matrix) M).det
source
@[simp]
theorem matrix.det_conj_transpose {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] [star_ring R] (M : matrix m m R) :
M.conj_transpose.det = has_star.star M.det

det_zero section #

Prove that a matrix with a repeated column has determinant equal to zero.

source
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
source
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
source
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.

source
theorem matrix.det_zero_of_column_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 : ∀ (k : n), M k i = M k j) :
M.det = 0

If a matrix has a repeated column, the determinant will be zero.

source
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
source
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
source
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
source
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
source
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) :
((s • M).update_row j u).det = s ^ (fintype.card n - 1) * (M.update_row j u).det
source
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) :
((s • M).update_column j u).det = s ^ (fintype.card n - 1) * (M.update_column j u).det

det_eq section #

Lemmas showing the determinant is invariant under a variety of operations.

source
theorem matrix.det_eq_of_eq_mul_det_one {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {A B : matrix n n R} (C : matrix n n R) (hC : C.det = 1) (hA : A = B.mul C) :
A.det = B.det
source
theorem matrix.det_eq_of_eq_det_one_mul {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {A B : matrix n n R} (C : matrix n n R) (hC : C.det = 1) (hA : A = C.mul B) :
A.det = B.det
source
theorem matrix.det_update_row_add_self {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) {i j : n} (hij : i ≠ j) :
(A.update_row i (A i + A j)).det = A.det
source
theorem matrix.det_update_column_add_self {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) {i j : n} (hij : i ≠ j) :
(A.update_column i (λ (k : n), A k i + A k j)).det = A.det
source
theorem matrix.det_update_row_add_smul_self {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :
(A.update_row i (A i + c • A j)).det = A.det
source
theorem matrix.det_update_column_add_smul_self {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :
(A.update_column i (λ (k : n), A k i + c • A k j)).det = A.det
source
theorem matrix.det_eq_of_forall_row_eq_smul_add_const_aux {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {A B : matrix n n R} {s : finset n} (c : n → R) (hs : ∀ (i : n), i ∉ s → c i = 0) (k : n) (hk : k ∉ s) (A_eq : ∀ (i j : n), A i j = B i j + c i * B k j) :
A.det = B.det
source
theorem matrix.det_eq_of_forall_row_eq_smul_add_const {n : Type u_2} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {A B : matrix n n R} (c : n → R) (k : n) (hk : c k = 0) (A_eq : ∀ (i j : n), A i j = B i j + c i * B k j) :
A.det = B.det

If you add multiples of row B k to other rows, the determinant doesn't change.

source
theorem matrix.det_eq_of_forall_row_eq_smul_add_pred_aux {R : Type v} [comm_ring R] {n : ℕ} (k : fin (n + 1)) (c : fin n → R) (hc : ∀ (i : fin n), k < i.succ → c i = 0) {M N : matrix (fin n.succ) (fin n.succ) R} (h0 : ∀ (j : fin n.succ), M 0 j = N 0 j) (hsucc : ∀ (i : fin n) (j : fin n.succ), M i.succ j = N i.succ j + c i * M (⇑fin.cast_succ i) j) :
M.det = N.det
source
theorem matrix.det_eq_of_forall_row_eq_smul_add_pred {R : Type v} [comm_ring R] {n : ℕ} {A B : matrix (fin (n + 1)) (fin (n + 1)) R} (c : fin n → R) (A_zero : ∀ (j : fin (n + 1)), A 0 j = B 0 j) (A_succ : ∀ (i : fin n) (j : fin (n + 1)), A i.succ j = B i.succ j + c i * A (⇑fin.cast_succ i) j) :
A.det = B.det

If you add multiples of previous rows to the next row, the determinant doesn't change.

source
theorem matrix.det_eq_of_forall_col_eq_smul_add_pred {R : Type v} [comm_ring R] {n : ℕ} {A B : matrix (fin (n + 1)) (fin (n + 1)) R} (c : fin n → R) (A_zero : ∀ (i : fin (n + 1)), A i 0 = B i 0) (A_succ : ∀ (i : fin (n + 1)) (j : fin n), A i j.succ = B i j.succ + c j * A i (⇑fin.cast_succ j)) :
A.det = B.det

If you add multiples of previous columns to the next columns, the determinant doesn't change.

source
@[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 = finset.univ.prod (λ (k : o), (M k).det)
source
@[simp]
theorem matrix.det_from_blocks_zero₂₁ {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) :
(matrix.from_blocks A B 0 D).det = A.det * D.det

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.

source
@[simp]
theorem matrix.det_from_blocks_zero₁₂ {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) (C : matrix n m R) (D : matrix n n R) :
(matrix.from_blocks A 0 C D).det = A.det * D.det

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.

source
theorem matrix.det_succ_column_zero {R : Type v} [comm_ring R] {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) :
A.det = finset.univ.sum (λ (i : fin n.succ), (-1) ^ ↑i * A i 0 * (A.submatrix ⇑(i.succ_above) fin.succ).det)

Laplacian expansion of the determinant of an n+1 × n+1 matrix along column 0.

source
theorem matrix.det_succ_row_zero {R : Type v} [comm_ring R] {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) :
A.det = finset.univ.sum (λ (j : fin n.succ), (-1) ^ ↑j * A 0 j * (A.submatrix fin.succ ⇑(j.succ_above)).det)

Laplacian expansion of the determinant of an n+1 × n+1 matrix along row 0.

source
theorem matrix.det_succ_row {R : Type v} [comm_ring R] {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) (i : fin n.succ) :
A.det = finset.univ.sum (λ (j : fin n.succ), (-1) ^ (↑i + ↑j) * A i j * (A.submatrix ⇑(i.succ_above) ⇑(j.succ_above)).det)

Laplacian expansion of the determinant of an n+1 × n+1 matrix along row i.

source
theorem matrix.det_succ_column {R : Type v} [comm_ring R] {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) (j : fin n.succ) :
A.det = finset.univ.sum (λ (i : fin n.succ), (-1) ^ (↑i + ↑j) * A i j * (A.submatrix ⇑(i.succ_above) ⇑(j.succ_above)).det)

Laplacian expansion of the determinant of an n+1 × n+1 matrix along column j.

source
@[simp]
theorem matrix.det_fin_zero {R : Type v} [comm_ring R] {A : matrix (fin 0) (fin 0) R} :
A.det = 1

Determinant of 0x0 matrix

source
theorem matrix.det_fin_one {R : Type v} [comm_ring R] (A : matrix (fin 1) (fin 1) R) :
A.det = A 0 0

Determinant of 1x1 matrix

source
theorem matrix.det_fin_one_of {R : Type v} [comm_ring R] (a : R) :
(⇑matrix.of ![![a]]).det = a
source
theorem matrix.det_fin_two {R : Type v} [comm_ring R] (A : matrix (fin 2) (fin 2) R) :
A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Determinant of 2x2 matrix

source
@[simp]
theorem matrix.det_fin_two_of {R : Type v} [comm_ring R] (a b c d : R) :
(⇑matrix.of ![![a, b], ![c, d]]).det = a * d - b * c
source
theorem matrix.det_fin_three {R : Type v} [comm_ring R] (A : matrix (fin 3) (fin 3) R) :
A.det = A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0

Determinant of 3x3 matrix