Metamath Proof Explorer

Table of Contents - 11.3. The determinant

1. Definition and basic properties
   1. cmdat
   2. df-mdet
   3. mdetfval
   4. mdetleib
   5. mdetleib2
   6. nfimdetndef
   7. mdetfval1
   8. mdetleib1
   9. mdet0pr
   10. mdet0f1o
   11. mdet0fv0
   12. mdetf
   13. mdetcl
   14. m1detdiag
   15. mdetdiaglem
   16. mdetdiag
   17. mdetdiagid
   18. mdet1
   19. mdetrlin
   20. mdetrsca
   21. mdetrsca2
   22. mdetr0
   23. mdet0
   24. mdetrlin2
   25. mdetralt
   26. mdetralt2
   27. mdetero
   28. mdettpos
   29. mdetunilem1
   30. mdetunilem2
   31. mdetunilem3
   32. mdetunilem4
   33. mdetunilem5
   34. mdetunilem6
   35. mdetunilem7
   36. mdetunilem8
   37. mdetunilem9
   38. mdetuni0
   39. mdetuni
   40. mdetmul
2. Determinants of 2 x 2 -matrices
   1. m2detleiblem1
   2. m2detleiblem5
   3. m2detleiblem6
   4. m2detleiblem7
   5. m2detleiblem2
   6. m2detleiblem3
   7. m2detleiblem4
   8. m2detleib
3. The matrix adjugate/adjunct
   1. cmadu
   2. cminmar1
   3. df-madu
   4. df-minmar1
   5. mndifsplit
   6. madufval
   7. maduval
   8. maducoeval
   9. maducoeval2
   10. maduf
   11. madutpos
   12. madugsum
   13. madurid
   14. madulid
   15. minmar1fval
   16. minmar1val0
   17. minmar1val
   18. minmar1eval
   19. minmar1marrep
   20. minmar1cl
   21. maducoevalmin1
4. Laplace expansion of determinants (special case)
   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
5. Inverse matrix
   1. invrvald
   2. matinv
   3. matunit
6. Cramer's rule
   1. slesolvec
   2. slesolinv
   3. slesolinvbi
   4. slesolex
   5. cramerimplem1
   6. cramerimplem2
   7. cramerimplem3
   8. cramerimp
   9. cramerlem1
   10. cramerlem2
   11. cramerlem3
   12. cramer0
   13. cramer