Metamath Proof Explorer

Table of Contents - 20.3.11. Matrices

1. Submatrices
   1. csmat
   2. df-smat
   3. smatfval
   4. smatrcl
   5. smatlem
   6. smattl
   7. smattr
   8. smatbl
   9. smatbr
   10. smatcl
   11. matmpo
   12. 1smat1
   13. submat1n
   14. submatres
   15. submateqlem1
   16. submateqlem2
   17. submateq
   18. submatminr1
2. Matrix literals
   1. clmat
   2. df-lmat
   3. lmatval
   4. lmatfval
   5. lmatfvlem
   6. lmatcl
   7. lmat22lem
   8. lmat22e11
   9. lmat22e12
   10. lmat22e21
   11. lmat22e22
   12. lmat22det
3. Laplace expansion of determinants
   1. mdetpmtr1
   2. mdetpmtr2
   3. mdetpmtr12
   4. mdetlap1
   5. madjusmdetlem1
   6. madjusmdetlem2
   7. madjusmdetlem3
   8. madjusmdetlem4
   9. madjusmdet
   10. mdetlap