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 = finset.univ.sum (λ (σ : equiv.perm n), ↑↑(⇑equiv.perm.sign σ) * finset.univ.prod (λ (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 = finset.univ.prod (λ (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 → finset.univ.sum (λ (σ : equiv.perm n), ↑↑(⇑equiv.perm.sign σ) * finset.univ.prod (λ (x : n), M (⇑σ x) (p x) * N (p x) x)) = 0
@[instance]
Equations
@[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_column_eq_zero
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
{A : matrix n n R}
(i : 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_column_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 column, 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