Metamath Proof Explorer


Table of Contents - 11.3.4. Laplace expansion of determinants (special case)

According to Wikipedia ("Laplace expansion", 08-Mar-2019, https://en.wikipedia.org/wiki/Laplace_expansion) "In linear algebra, the Laplace expansion, named after Pierre-Simon Laplace, also called cofactor expansion, is an expression for the determinant det(B) of an n x n -matrix B that is a weighted sum of the determinants of n sub-matrices of B, each of size (n-1) x (n-1)". The expansion is usually performed for a row of matrix B (alternately for a column of matrix B). The mentioned "sub-matrices" are the matrices resultung from deleting the i-th row and the j-th column of matrix B. The mentioned "weights" (factors/coefficients) are the elements at position i and j in matrix B. If the expansion is performed for a row, the coefficients are the elements of the selected row.

In the following, only the case where the row for the expansion contains only the zero element of the underlying ring except at the diagonal position. By this, the sum for the Laplace expansion is reduced to one summand, consisting of the element at the diagonal position multiplied with the determinant of the corresponding submatrix, see smadiadetg or smadiadetr.

  1. symgmatr01lem
  2. symgmatr01
  3. gsummatr01lem1
  4. gsummatr01lem2
  5. gsummatr01lem3
  6. gsummatr01lem4
  7. gsummatr01
  8. marep01ma
  9. smadiadetlem0
  10. smadiadetlem1
  11. smadiadetlem1a
  12. smadiadetlem2
  13. smadiadetlem3lem0
  14. smadiadetlem3lem1
  15. smadiadetlem3lem2
  16. smadiadetlem3
  17. smadiadetlem4
  18. smadiadet
  19. smadiadetglem1
  20. smadiadetglem2
  21. smadiadetg
  22. smadiadetg0
  23. smadiadetr