Documentation

Mathlib.LinearAlgebra.Matrix.Determinant

Determinant of a matrix #

This file defines the determinant of a matrix, Matrix.det, and its essential properties.

Main definitions #

Main results #

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] :
(nR) [Λ^n]→ₗ[R] R

det is an AlternatingMap in the rows of the matrix.

Equations
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
    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 n) => Equiv.Perm.sign σ Finset.prod Finset.univ fun (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) :
      Matrix.det M = Finset.sum Finset.univ fun (σ : Equiv.Perm n) => (Equiv.Perm.sign σ) * Finset.prod Finset.univ fun (i : n) => M (σ i) i
      @[simp]
      theorem Matrix.det_diagonal {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {d : nR} :
      Matrix.det (Matrix.diagonal d) = Finset.prod Finset.univ fun (i : n) => d i
      theorem Matrix.det_zero {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
      @[simp]
      theorem Matrix.det_one {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
      theorem Matrix.det_isEmpty {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [IsEmpty n] {A : Matrix n n R} :
      @[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) :
      @[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 : nn} (H : ¬Function.Bijective p) :
      (Finset.sum Finset.univ fun (σ : Equiv.Perm n) => (Equiv.Perm.sign σ) * Finset.prod Finset.univ fun (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 : Matrix n n R) (N : Matrix n n R) :
      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.

      Equations
      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)

        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 : 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 : n) => 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) :

        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) :

        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) :
        @[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) :
        theorem Matrix.det_neg {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) :
        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 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 : nR) (A : Matrix n n R) :
        Matrix.det (Matrix.of fun (i j : n) => v j * A i j) = (Finset.prod Finset.univ fun (i : n) => 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 : nR) (A : Matrix n n R) :
        Matrix.det (Matrix.of fun (i j : n) => v i * A i j) = (Finset.prod Finset.univ fun (i : n) => 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 : ) :
        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) :
        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) :
        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) :
        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) :
        @[simp]

        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) :
        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) :
        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) :

        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) :

        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 : nR) (v : nR) :
        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 : nR) (v : nR) :
        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 : nR) :
        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 : nR) :
        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 : nR) :
        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 : nR) :

        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) :
        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) :
        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) :
        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 : n) => 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) :
        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 : n) => 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 : nR) :
        (is, c i = 0)ks, (∀ (i j : n), A i j = B i j + c i * B k j)Matrix.det A = Matrix.det B
        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 : nR) (k : n) (hk : c k = 0) (A_eq : ∀ (i j : n), A i j = B i j + c i * B k j) :

        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 nR) (_hc : ∀ (i : Fin n), k < Fin.succ ic 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) :
        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 nR) (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) :

        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 nR) (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)) :

        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 : oMatrix n n R) :
        Matrix.det (Matrix.blockDiagonal M) = Finset.prod Finset.univ fun (k : o) => 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) :

        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) :

        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 : Fin (Nat.succ n)) => (-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 : Fin (Nat.succ n)) => (-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 : Fin (Nat.succ n)) => (-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 : Fin (Nat.succ n)) => (-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} :

        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
        theorem Matrix.det_fin_two {R : Type v} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) :
        Matrix.det A = 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 : R) (b : R) (c : R) (d : R) :
        Matrix.det (Matrix.of ![![a, b], ![c, d]]) = a * d - b * c
        theorem Matrix.det_fin_three {R : Type v} [CommRing R] (A : Matrix (Fin 3) (Fin 3) R) :
        Matrix.det A = 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