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 permutations
• Matrix.detRowAlternating: the determinant, as an AlternatingMap in the rows of the matrix

Main results

• det_mul: the determinant of A * B is the product of determinants
• det_zero_of_row_eq: the determinant is zero if there is a repeated row
• det_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 MathlibTest/matrix.lean for some examples.

def Matrix.detRowAlternating {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : (n → R) [⋀^n]→ₗ[R] R

det is an AlternatingMap in the rows of the matrix.

def 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.

theorem Matrix.det_apply {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing 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} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) : M.det = ∑ σ : Equiv.Perm n, ↑↑(Equiv.Perm.sign σ) * ∏ i : n, M (σ i) i

theorem Matrix.det_eq_detp_sub_detp {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) : M.det = detp 1 M - detp (-1) M

@[simp]

theorem Matrix.det_diagonal {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {d : n → R} : (diagonal d).det = ∏ i : n, d i

theorem Matrix.det_zero {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Nonempty n → det 0 = 0

@[simp]

theorem Matrix.det_one {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : 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} : A.det = 1

@[simp]

theorem Matrix.coe_det_isEmpty {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [IsEmpty n] : 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) : A.det = 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) : A.det = 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) : A.det = 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) : A.det = A k k

theorem Matrix.det_mul_aux {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing 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

@[simp]

theorem Matrix.det_mul {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M N : Matrix n n R) : (M * N).det = M.det * N.det

def Matrix.detMonoidHom {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Matrix n n R →* R

The determinant of a matrix, as a monoid homomorphism.

@[simp]

theorem Matrix.coe_detMonoidHom {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : ⇑detMonoidHom = det

theorem Matrix.det_mul_comm {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] (M N : Matrix m m R) : (M * N).det = (N * M).det

On square matrices, mul_comm applies under det.

theorem Matrix.det_mul_left_comm {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] (M N P : Matrix m m R) : (M * (N * P)).det = (N * (M * P)).det

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 N P : Matrix m m R) : (M * N * P).det = (M * P * N).det

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) : (↑M * N * ↑M⁻¹).det = N.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) : (↑M⁻¹ * N * ↑M).det = N.det

@[simp]

theorem Matrix.det_transpose {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) : M.transpose.det = M.det

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) : (M.submatrix (⇑σ) id).det = ↑↑(Equiv.Perm.sign σ) * M.det

Permuting the columns changes the sign of 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) : (M.submatrix id ⇑σ).det = ↑↑(Equiv.Perm.sign σ) * M.det

Permuting the rows 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) : (A.submatrix ⇑e ⇑e).det = A.det

Permuting rows and columns with the same equivalence does not change the determinant.

@[simp]

theorem Matrix.abs_det_submatrix_equiv_equiv {m : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] {R : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (e₁ e₂ : n ≃ m) (A : Matrix m m R) : |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Permuting rows and columns with two equivalences does not change the absolute value of the determinant.

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) : ((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_submatrix_equiv_self; this one is unsuitable because Matrix.reindex_apply unfolds reindex first.

theorem Matrix.det_reindex {m : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] (e e' : m ≃ n) (M : Matrix m m R) : ((reindex e e') M).det = ↑↑(Equiv.Perm.sign (e'.trans e.symm)) * M.det

theorem Matrix.abs_det_reindex {m : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] {R : Type u_3} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (e₁ e₂ : m ≃ n) (A : Matrix m m R) : |((reindex e₁ e₂) A).det| = |A.det|

Reindexing both indices along equivalences preserves the absolute of the determinant.

For the simp version of this lemma, see abs_det_submatrix_equiv_equiv; this one is unsuitable because Matrix.reindex_apply unfolds reindex first.

theorem Matrix.det_smul {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (c : R) : (c • A).det = c ^ Fintype.card n * A.det

@[simp]

theorem Matrix.det_smul_of_tower {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {α : Type u_3} [Monoid α] [MulAction α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : α) (A : Matrix n n R) : (c • A).det = c ^ Fintype.card n • A.det

theorem Matrix.det_neg {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) : (-A).det = (-1) ^ Fintype.card n * A.det

theorem Matrix.det_neg_eq_smul {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) : (-A).det = (-1) ^ Fintype.card n • A.det

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) : (of fun (i j : n) => v j * A i j).det = (∏ 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} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (v : n → R) (A : Matrix n n R) : (of fun (i j : n) => v i * A i j).det = (∏ i : n, v i) * A.det

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 : ℕ) : (M ^ n).det = M.det ^ 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 M.det = (f.mapMatrix M).det

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 M.det = (f.mapMatrix M).det

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 M.det = (f.mapMatrix M).det

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 M.det = (f.mapMatrix M).det

theorem Int.cast_det {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n ℤ) : ↑M.det = (M.map fun (x : ℤ) => ↑x).det

theorem Rat.cast_det {n : Type u_2} [DecidableEq n] [Fintype n] {F : Type u_3} [Field F] [CharZero F] (M : Matrix n n ℚ) : ↑M.det = (M.map fun (x : ℚ) => ↑x).det

@[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) : M.conjTranspose.det = star M.det

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} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {A : Matrix n n R} (i : n) (h : ∀ (j : n), A i j = 0) : A.det = 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) : A.det = 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 j : n} (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 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 j : n} (i_ne_j : i ≠ j) (hij : ∀ (k : n), M k i = M k j) : M.det = 0

If a matrix has a repeated column, the determinant will be zero.

theorem Matrix.det_updateRow_eq_zero {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {M : Matrix n n R} {i j : n} (h : i ≠ j) : (M.updateRow j (M i)).det = 0

If we repeat a row of a matrix, we get a matrix of determinant zero.

theorem Matrix.det_updateCol_eq_zero {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {M : Matrix n n R} {i j : n} (h : i ≠ j) : (M.updateCol j fun (k : n) => M k i).det = 0

If we repeat a column of a matrix, we get a matrix of determinant 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 v : n → R) : (M.updateRow j (u + v)).det = (M.updateRow j u).det + (M.updateRow j v).det

theorem Matrix.det_updateCol_add {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) (j : n) (u v : n → R) : (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

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) : (M.updateRow j (s • u)).det = s * (M.updateRow j u).det

theorem Matrix.det_updateCol_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) : (M.updateCol j (s • u)).det = s * (M.updateCol j u).det

theorem Matrix.det_updateRow_smul_left {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) : ((s • M).updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateRow j u).det

theorem Matrix.det_updateCol_smul_left {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) : ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

theorem Matrix.det_updateRow_sum_aux {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n R) {j : n} (s : Finset n) (hj : j ∉ s) (c : n → R) (a : R) : (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det

theorem Matrix.det_updateRow_sum {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (j : n) (c : n → R) : (A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det

If we replace a row of a matrix by a linear combination of its rows, then the determinant is multiplied by the coefficient of that row.

theorem Matrix.det_updateCol_sum {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (j : n) (c : n → R) : (A.updateCol j fun (k : n) => ∑ i : n, c i • A k i).det = c j • A.det

If we replace a column of a matrix by a linear combination of its columns, then the determinant is multiplied by the coefficient of that column.

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 B : Matrix n n R} (C : Matrix n n R) (hC : C.det = 1) (hA : A = B * C) : A.det = B.det

theorem Matrix.det_eq_of_eq_det_one_mul {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {A B : Matrix n n R} (C : Matrix n n R) (hC : C.det = 1) (hA : A = C * B) : A.det = B.det

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 j : n} (hij : i ≠ j) : (A.updateRow i (A i + A j)).det = A.det

theorem Matrix.det_updateCol_add_self {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) {i j : n} (hij : i ≠ j) : (A.updateCol i fun (k : n) => A k i + A k j).det = A.det

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 j : n} (hij : i ≠ j) (c : R) : (A.updateRow i (A i + c • A j)).det = A.det

theorem Matrix.det_updateCol_add_smul_self {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) : (A.updateCol i fun (k : n) => A k i + c • A k j).det = A.det

theorem Matrix.det_eq_zero_of_not_linearIndependent_rows {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] [IsDomain R] {A : Matrix m m R} (hA : ¬LinearIndependent R fun (i : m) => A i) : A.det = 0

theorem Matrix.linearIndependent_rows_of_det_ne_zero {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) : LinearIndependent R fun (i : m) => A i

theorem Matrix.linearIndependent_cols_of_det_ne_zero {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) : LinearIndependent R A.col

theorem Matrix.det_eq_zero_of_not_linearIndependent_cols {m : Type u_1} [DecidableEq m] [Fintype m] {R : Type v} [CommRing R] [IsDomain R] {A : Matrix m m R} (hA : ¬LinearIndependent R fun (i : m) => A.transpose i) : A.det = 0

theorem Matrix.det_vecMulVec {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Nontrivial n] (u v : n → R) : (vecMulVec u v).det = 0

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 B : Matrix n n R} {s : Finset n} (c : n → R) : (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det

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 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) : A.det = B.det

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 < 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 i.castSucc j) : M.det = N.det

theorem Matrix.det_eq_of_forall_row_eq_smul_add_pred {R : Type v} [CommRing 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 i.castSucc j) : A.det = B.det

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 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 j.castSucc) : A.det = B.det

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) : (blockDiagonal M).det = ∏ k : o, (M k).det

@[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) : (fromBlocks A B 0 D).det = A.det * D.det

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_upperTriangular.

@[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) : (fromBlocks A 0 C D).det = A.det * D.det

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_lowerTriangular.

theorem Matrix.det_succ_column_zero {R : Type v} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) : A.det = ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

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 n.succ) (Fin n.succ) R) : A.det = ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

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 n.succ) (Fin n.succ) R) (i : Fin n.succ) : A.det = ∑ j : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

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 n.succ) (Fin n.succ) R) (j : Fin n.succ) : A.det = ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

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} : A.det = 1

Determinant of 0x0 matrix

theorem Matrix.det_fin_one {R : Type v} [CommRing R] (A : Matrix (Fin 1) (Fin 1) R) : A.det = A 0 0

Determinant of 1x1 matrix

theorem Matrix.det_fin_one_of {R : Type v} [CommRing R] (a : R) : !![a].det = a

theorem Matrix.det_fin_two {R : Type v} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) : A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Determinant of 2x2 matrix

@[simp]

theorem Matrix.det_fin_two_of {R : Type v} [CommRing R] (a b c d : R) : !![a, b; c, d].det = a * d - b * c

theorem Matrix.det_fin_three {R : Type v} [CommRing R] (A : Matrix (Fin 3) (Fin 3) R) : A.det = A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0

Determinant of 3x3 matrix