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_alternating: 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_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.
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_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} :
@[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
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_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) :
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
The determinant of a matrix, as a monoid homomorphism.
Equations
- matrix.det_monoid_hom = {to_fun := matrix.det _inst_5, map_one' := _, map_mul' := _}
@[simp]
theorem
matrix.coe_det_monoid_hom
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
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) :
On square matrices, mul_left_comm applies under det.
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) :
On square matrices, mul_right_comm applies under det.
@[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.
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) :
@[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) :
theorem
matrix.det_neg
{n : Type u_2}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(A : matrix n n R) :
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 variant of matrix.det_neg with scalar multiplication by units ℤ instead of multiplication
by R.
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.det (λ (i j : n), (v j) * A i j) = (∏ (i : n), v i) * A.det
Multiplying each row by a fixed v i multiplies the determinant by
the product of the vs.
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.det (λ (i j : n), (v i) * A i j) = (∏ (i : n), v i) * A.det
Multiplying each column by a fixed v j multiplies the determinant by
the product of the vs.
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) :
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) :
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_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) :
If a matrix has a repeated column, 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
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
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.
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
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
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) :
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) :
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) :
If you add multiples of row B k to other rows, the determinant doesn't change.
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) :
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) :
If you add multiples of previous rows to the next row, the determinant doesn't change.
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)) :
If you add multiples of previous columns to the next columns, the determinant doesn't change.
@[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
@[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) :
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.
@[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) :
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.