def
matrix.det
{n : Type u}
[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.
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]
theorem
matrix.det_zero
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(h : nonempty n) :
@[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}
(h : fintype.card n = 0) :
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}
(H : ¬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)
(h : ∀ (j : n), A i j = 0) :
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)
(h : ∀ (i : n), A i j = 0) :
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}
(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_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_row_multilinear_apply
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(M : matrix n n R) :
def
matrix.det_row_multilinear
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
alternating_map R (n → R) R n
det is an alternating multilinear map over the rows of the matrix.
See also is_basis.det.
Equations
- matrix.det_row_multilinear = {to_fun := matrix.det _inst_3, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[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