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.detRowAlternating: the determinant, as anAlternatingMapin 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.detRowAlternating
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
:
AlternatingMap R (n → R) R n
det is an AlternatingMap in the rows of the matrix.
Equations
- Matrix.detRowAlternating = ↑MultilinearMap.alternatization (MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebra R n R) LinearMap.proj)
Instances For
@[inline, reducible]
abbrev
Matrix.det
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
:
R
The determinant of a matrix given by the Leibniz formula.
Equations
- Matrix.det M = ↑Matrix.detRowAlternating M
Instances For
theorem
Matrix.det_apply
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
:
Matrix.det M = Finset.sum Finset.univ fun σ => ↑Equiv.Perm.sign σ • Finset.prod Finset.univ fun i => M (↑σ i) i
theorem
Matrix.det_apply'
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
:
Matrix.det M = Finset.sum Finset.univ fun σ => ↑↑(↑Equiv.Perm.sign σ) * Finset.prod Finset.univ fun i => M (↑σ i) i
@[simp]
theorem
Matrix.det_diagonal
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{d : n → R}
:
Matrix.det (Matrix.diagonal d) = Finset.prod Finset.univ fun i => d i
theorem
Matrix.det_zero
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
:
Nonempty n → Matrix.det 0 = 0
@[simp]
theorem
Matrix.det_one
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
:
Matrix.det 1 = 1
theorem
Matrix.det_isEmpty
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
[IsEmpty n]
{A : Matrix n n R}
:
Matrix.det A = 1
@[simp]
theorem
Matrix.coe_det_isEmpty
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
[IsEmpty n]
:
Matrix.det = Function.const (Matrix n n R) 1
theorem
Matrix.det_eq_one_of_card_eq_zero
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
(h : Fintype.card n = 0)
:
Matrix.det A = 1
@[simp]
theorem
Matrix.det_unique
{R : Type v}
[CommRing R]
{n : Type u_3}
[Unique n]
[DecidableEq n]
[Fintype n]
(A : Matrix n n R)
:
Matrix.det A = A default default
If n has only one element, the determinant of an n by n matrix is just that element.
Although Unique implies DecidableEq 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}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
[Subsingleton n]
(A : Matrix n n R)
(k : n)
:
Matrix.det A = A k k
theorem
Matrix.det_eq_elem_of_card_eq_one
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
(h : Fintype.card n = 1)
(k : n)
:
Matrix.det A = A k k
theorem
Matrix.det_mul_aux
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{M : Matrix n n R}
{N : Matrix n n R}
{p : n → n}
(H : ¬Function.Bijective p)
:
(Finset.sum Finset.univ fun σ => ↑↑(↑Equiv.Perm.sign σ) * Finset.prod Finset.univ fun x => M (↑σ x) (p x) * N (p x) x) = 0
@[simp]
theorem
Matrix.det_mul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(N : Matrix n n R)
:
Matrix.det (M * N) = Matrix.det M * Matrix.det N
The determinant of a matrix, as a monoid homomorphism.
Equations
- Matrix.detMonoidHom = { toOneHom := { toFun := Matrix.det, map_one' := (_ : Matrix.det 1 = 1) }, map_mul' := (_ : ∀ (M N : Matrix n n R), Matrix.det (M * N) = Matrix.det M * Matrix.det N) }
Instances For
@[simp]
theorem
Matrix.coe_detMonoidHom
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
:
↑Matrix.detMonoidHom = Matrix.det
theorem
Matrix.det_mul_comm
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : Matrix m m R)
(N : Matrix m m R)
:
Matrix.det (M * N) = Matrix.det (N * M)
theorem
Matrix.det_mul_left_comm
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : Matrix m m R)
(N : Matrix m m R)
(P : Matrix m m R)
:
Matrix.det (M * (N * P)) = Matrix.det (N * (M * P))
On square matrices, mul_left_comm applies under det.
theorem
Matrix.det_mul_right_comm
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : Matrix m m R)
(N : Matrix m m R)
(P : Matrix m m R)
:
Matrix.det (M * N * P) = Matrix.det (M * P * N)
On square matrices, mul_right_comm applies under det.
theorem
Matrix.det_units_conj
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : (Matrix m m R)ˣ)
(N : Matrix m m R)
:
Matrix.det (↑M * N * ↑M⁻¹) = Matrix.det N
theorem
Matrix.det_units_conj'
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : (Matrix m m R)ˣ)
(N : Matrix m m R)
:
Matrix.det (↑M⁻¹ * N * ↑M) = Matrix.det N
@[simp]
theorem
Matrix.det_transpose
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
:
Transposing a matrix preserves the determinant.
theorem
Matrix.det_permute
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(σ : Equiv.Perm n)
(M : Matrix n n R)
:
(Matrix.det fun i => M (↑σ i)) = ↑↑(↑Equiv.Perm.sign σ) * Matrix.det M
Permuting the columns changes the sign of the determinant.
@[simp]
theorem
Matrix.det_submatrix_equiv_self
{m : Type u_1}
{n : Type u_2}
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(e : n ≃ m)
(A : Matrix m m R)
:
Matrix.det (Matrix.submatrix A ↑e ↑e) = Matrix.det A
Permuting rows and columns with the same equivalence has no effect.
theorem
Matrix.det_reindex_self
{m : Type u_1}
{n : Type u_2}
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(e : m ≃ n)
(A : Matrix m m R)
:
Matrix.det (↑(Matrix.reindex e e) A) = Matrix.det A
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.
@[simp]
theorem
Matrix.det_permutation
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(σ : Equiv.Perm n)
:
Matrix.det (PEquiv.toMatrix (Equiv.toPEquiv σ)) = ↑↑(↑Equiv.Perm.sign σ)
The determinant of a permutation matrix equals its sign.
theorem
Matrix.det_smul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
(c : R)
:
Matrix.det (c • A) = c ^ Fintype.card n * Matrix.det A
@[simp]
theorem
Matrix.det_smul_of_tower
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{α : Type u_3}
[Monoid α]
[DistribMulAction α R]
[IsScalarTower α R R]
[SMulCommClass α R R]
(c : α)
(A : Matrix n n R)
:
Matrix.det (c • A) = c ^ Fintype.card n • Matrix.det A
theorem
Matrix.det_neg
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
:
Matrix.det (-A) = (-1) ^ Fintype.card n * Matrix.det A
theorem
Matrix.det_neg_eq_smul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
:
Matrix.det (-A) = (-1) ^ Fintype.card n • Matrix.det A
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}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(v : n → R)
(A : Matrix n n R)
:
Matrix.det (↑Matrix.of fun i j => v j * A i j) = (Finset.prod Finset.univ fun i => v i) * Matrix.det A
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}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(v : n → R)
(A : Matrix n n R)
:
Matrix.det (↑Matrix.of fun i j => v i * A i j) = (Finset.prod Finset.univ fun i => v i) * Matrix.det A
Multiplying each column by a fixed v j multiplies the determinant by
the product of the vs.
@[simp]
theorem
Matrix.det_pow
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(M : Matrix m m R)
(n : ℕ)
:
Matrix.det (M ^ n) = Matrix.det M ^ n
theorem
RingHom.map_det
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{S : Type w}
[CommRing S]
(f : R →+* S)
(M : Matrix n n R)
:
↑f (Matrix.det M) = Matrix.det (↑(RingHom.mapMatrix f) M)
theorem
RingEquiv.map_det
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{S : Type w}
[CommRing S]
(f : R ≃+* S)
(M : Matrix n n R)
:
↑f (Matrix.det M) = Matrix.det (↑(RingEquiv.mapMatrix f) M)
theorem
AlgHom.map_det
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{S : Type w}
[CommRing S]
[Algebra R S]
{T : Type z}
[CommRing T]
[Algebra R T]
(f : S →ₐ[R] T)
(M : Matrix n n S)
:
↑f (Matrix.det M) = Matrix.det (↑(AlgHom.mapMatrix f) M)
theorem
AlgEquiv.map_det
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{S : Type w}
[CommRing S]
[Algebra R S]
{T : Type z}
[CommRing T]
[Algebra R T]
(f : S ≃ₐ[R] T)
(M : Matrix n n S)
:
↑f (Matrix.det M) = Matrix.det (↑(AlgEquiv.mapMatrix f) M)
@[simp]
theorem
Matrix.det_conjTranspose
{m : Type u_1}
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
[StarRing R]
(M : Matrix m m R)
:
Matrix.det (Matrix.conjTranspose M) = star (Matrix.det M)
theorem
Matrix.det_eq_zero_of_row_eq_zero
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
(i : n)
(h : ∀ (j : n), A i j = 0)
:
Matrix.det A = 0
theorem
Matrix.det_eq_zero_of_column_eq_zero
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
(j : n)
(h : ∀ (i : n), A i j = 0)
:
Matrix.det A = 0
theorem
Matrix.det_zero_of_row_eq
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{M : Matrix n n R}
{i : n}
{j : n}
(i_ne_j : i ≠ j)
(hij : M i = M j)
:
Matrix.det M = 0
If a matrix has a repeated row, the determinant will be zero.
theorem
Matrix.det_zero_of_column_eq
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{M : Matrix n n R}
{i : n}
{j : n}
(i_ne_j : i ≠ j)
(hij : ∀ (k : n), M k i = M k j)
:
Matrix.det M = 0
If a matrix has a repeated column, the determinant will be zero.
theorem
Matrix.det_updateRow_add
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(u : n → R)
(v : n → R)
:
Matrix.det (Matrix.updateRow M j (u + v)) = Matrix.det (Matrix.updateRow M j u) + Matrix.det (Matrix.updateRow M j v)
theorem
Matrix.det_updateColumn_add
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(u : n → R)
(v : n → R)
:
Matrix.det (Matrix.updateColumn M j (u + v)) = Matrix.det (Matrix.updateColumn M j u) + Matrix.det (Matrix.updateColumn M j v)
theorem
Matrix.det_updateRow_smul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(s : R)
(u : n → R)
:
Matrix.det (Matrix.updateRow M j (s • u)) = s * Matrix.det (Matrix.updateRow M j u)
theorem
Matrix.det_updateColumn_smul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(s : R)
(u : n → R)
:
Matrix.det (Matrix.updateColumn M j (s • u)) = s * Matrix.det (Matrix.updateColumn M j u)
theorem
Matrix.det_updateRow_smul'
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(s : R)
(u : n → R)
:
Matrix.det (Matrix.updateRow (s • M) j u) = s ^ (Fintype.card n - 1) * Matrix.det (Matrix.updateRow M j u)
theorem
Matrix.det_updateColumn_smul'
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(M : Matrix n n R)
(j : n)
(s : R)
(u : n → R)
:
Matrix.det (Matrix.updateColumn (s • M) j u) = s ^ (Fintype.card n - 1) * Matrix.det (Matrix.updateColumn M j u)
det_eq section #
Lemmas showing the determinant is invariant under a variety of operations.
theorem
Matrix.det_eq_of_eq_mul_det_one
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
{B : Matrix n n R}
(C : Matrix n n R)
(hC : Matrix.det C = 1)
(hA : A = B * C)
:
Matrix.det A = Matrix.det B
theorem
Matrix.det_eq_of_eq_det_one_mul
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
{B : Matrix n n R}
(C : Matrix n n R)
(hC : Matrix.det C = 1)
(hA : A = C * B)
:
Matrix.det A = Matrix.det B
theorem
Matrix.det_updateRow_add_self
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
{i : n}
{j : n}
(hij : i ≠ j)
:
Matrix.det (Matrix.updateRow A i (A i + A j)) = Matrix.det A
theorem
Matrix.det_updateColumn_add_self
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
{i : n}
{j : n}
(hij : i ≠ j)
:
Matrix.det (Matrix.updateColumn A i fun k => A k i + A k j) = Matrix.det A
theorem
Matrix.det_updateRow_add_smul_self
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
{i : n}
{j : n}
(hij : i ≠ j)
(c : R)
:
Matrix.det (Matrix.updateRow A i (A i + c • A j)) = Matrix.det A
theorem
Matrix.det_updateColumn_add_smul_self
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
(A : Matrix n n R)
{i : n}
{j : n}
(hij : i ≠ j)
(c : R)
:
Matrix.det (Matrix.updateColumn A i fun k => A k i + c • A k j) = Matrix.det A
theorem
Matrix.det_eq_of_forall_row_eq_smul_add_const_aux
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
{B : Matrix n n R}
{s : Finset n}
(c : n → R)
:
theorem
Matrix.det_eq_of_forall_row_eq_smul_add_const
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{A : Matrix n n R}
{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)
:
Matrix.det A = Matrix.det B
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}
[CommRing R]
{n : ℕ}
(k : Fin (n + 1))
(c : Fin n → R)
(_hc : ∀ (i : Fin n), k < Fin.succ i → c i = 0)
{M : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R}
{N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R}
(_h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j)
(_hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (Fin.castSucc i) j)
:
Matrix.det M = Matrix.det N
theorem
Matrix.det_eq_of_forall_row_eq_smul_add_pred
{R : Type v}
[CommRing R]
{n : ℕ}
{A : Matrix (Fin (n + 1)) (Fin (n + 1)) R}
{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 (Fin.succ i) j = B (Fin.succ i) j + c i * A (Fin.castSucc i) j)
:
Matrix.det A = Matrix.det B
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}
[CommRing R]
{n : ℕ}
{A : Matrix (Fin (n + 1)) (Fin (n + 1)) R}
{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 (Fin.succ j) = B i (Fin.succ j) + c j * A i (Fin.castSucc j))
:
Matrix.det A = Matrix.det B
If you add multiples of previous columns to the next columns, the determinant doesn't change.
@[simp]
theorem
Matrix.det_blockDiagonal
{n : Type u_2}
[DecidableEq n]
[Fintype n]
{R : Type v}
[CommRing R]
{o : Type u_3}
[Fintype o]
[DecidableEq o]
(M : o → Matrix n n R)
:
Matrix.det (Matrix.blockDiagonal M) = Finset.prod Finset.univ fun k => Matrix.det (M k)
@[simp]
theorem
Matrix.det_fromBlocks_zero₂₁
{m : Type u_1}
{n : Type u_2}
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(A : Matrix m m R)
(B : Matrix m n R)
(D : Matrix n n R)
:
Matrix.det (Matrix.fromBlocks A B 0 D) = Matrix.det A * Matrix.det D
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_fromBlocks_zero₁₂
{m : Type u_1}
{n : Type u_2}
[DecidableEq n]
[Fintype n]
[DecidableEq m]
[Fintype m]
{R : Type v}
[CommRing R]
(A : Matrix m m R)
(C : Matrix n m R)
(D : Matrix n n R)
:
Matrix.det (Matrix.fromBlocks A 0 C D) = Matrix.det A * Matrix.det D
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.
theorem
Matrix.det_succ_column_zero
{R : Type v}
[CommRing R]
{n : ℕ}
(A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R)
:
Matrix.det A = Finset.sum Finset.univ fun i => (-1) ^ ↑i * A i 0 * Matrix.det (Matrix.submatrix A (Fin.succAbove i) Fin.succ)
Laplacian expansion of the determinant of an n+1 × n+1 matrix along column 0.
theorem
Matrix.det_succ_row_zero
{R : Type v}
[CommRing R]
{n : ℕ}
(A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R)
:
Matrix.det A = Finset.sum Finset.univ fun j => (-1) ^ ↑j * A 0 j * Matrix.det (Matrix.submatrix A Fin.succ (Fin.succAbove j))
Laplacian expansion of the determinant of an n+1 × n+1 matrix along row 0.
theorem
Matrix.det_succ_row
{R : Type v}
[CommRing R]
{n : ℕ}
(A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R)
(i : Fin (Nat.succ n))
:
Matrix.det A = Finset.sum Finset.univ fun j =>
(-1) ^ (↑i + ↑j) * A i j * Matrix.det (Matrix.submatrix A (Fin.succAbove i) (Fin.succAbove j))
Laplacian expansion of the determinant of an n+1 × n+1 matrix along row i.
theorem
Matrix.det_succ_column
{R : Type v}
[CommRing R]
{n : ℕ}
(A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R)
(j : Fin (Nat.succ n))
:
Matrix.det A = Finset.sum Finset.univ fun i =>
(-1) ^ (↑i + ↑j) * A i j * Matrix.det (Matrix.submatrix A (Fin.succAbove i) (Fin.succAbove j))
Laplacian expansion of the determinant of an n+1 × n+1 matrix along column j.
@[simp]
theorem
Matrix.det_fin_zero
{R : Type v}
[CommRing R]
{A : Matrix (Fin 0) (Fin 0) R}
:
Matrix.det A = 1
Determinant of 0x0 matrix
theorem
Matrix.det_fin_one
{R : Type v}
[CommRing R]
(A : Matrix (Fin 1) (Fin 1) R)
:
Matrix.det A = A 0 0
Determinant of 1x1 matrix
theorem
Matrix.det_fin_one_of
{R : Type v}
[CommRing R]
(a : R)
:
Matrix.det (↑Matrix.of ![![a]]) = a
@[simp]
theorem
Matrix.det_fin_two_of
{R : Type v}
[CommRing R]
(a : R)
(b : R)
(c : R)
(d : R)
:
Matrix.det (↑Matrix.of ![![a, b], ![c, d]]) = a * d - b * c