def
matrix.det
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
matrix n n R → R
The determinant of a matrix given by the Leibniz formula.
Equations
- M.det = ∑ (σ : equiv.perm n), (↑↑(⇑equiv.perm.sign σ)) * ∏ (i : n), M (⇑σ i) i
@[simp]
theorem
matrix.det_diagonal
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{d : n → R} :
(matrix.diagonal d).det = ∏ (i : n), d i
@[simp]
@[simp]
theorem
matrix.det_eq_one_of_card_eq_zero
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R} :
fintype.card n = 0 → A.det = 1
theorem
matrix.det_mul_aux
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{M N : matrix n n R}
{p : n → n} :
¬function.bijective p → ∑ (σ : equiv.perm n), (↑↑(⇑equiv.perm.sign σ)) * ∏ (x : n), (M (⇑σ x) (p x)) * N (p x) x = 0
@[instance]
@[simp]
theorem
matrix.det_transpose
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
Transposing a matrix preserves the determinant.
@[simp]
theorem
matrix.det_permutation
{n : Type u}
[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_permute
{n : Type u}
[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_smul
{n : Type u}
[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}
[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}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(i : n) :
theorem
matrix.det_eq_zero_of_column_eq_zero
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(j : n) :
mod_swap i j contains permutations up to swapping i and j.
We use this to partition permutations in the expression for the determinant,
such that each partitions sums up to 0.
Equations
- matrix.mod_swap i j = {r := λ (σ τ : equiv.perm n), σ = τ ∨ σ = (equiv.swap i j) * τ, iseqv := _}
@[instance]
Equations
- matrix.decidable_rel i j = λ (σ τ : equiv.perm n), or.decidable
theorem
matrix.det_zero_of_row_eq
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{M : matrix n n R}
{i j : n} :
If a matrix has a repeated row, the determinant will be zero.
theorem
matrix.det_update_column_add
{n : Type u}
[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_add
{n : Type u}
[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_smul
{n : Type u}
[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}
[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
@[simp]
theorem
matrix.det_block_diagonal
{n : Type u}
[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