Metamath Proof Explorer
Table of Contents - 11.5. The determinant
- Definition and basic properties
- cmdat
- df-mdet
- mdetfval
- mdetleib
- mdetleib2
- nfimdetndef
- mdetfval1
- mdetleib1
- mdet0pr
- mdet0f1o
- mdet0fv0
- mdetf
- mdetcl
- m1detdiag
- mdetdiaglem
- mdetdiag
- mdetdiagid
- mdet1
- mdetrlin
- mdetrsca
- mdetrsca2
- mdetr0
- mdet0
- mdetrlin2
- mdetralt
- mdetralt2
- mdetero
- mdettpos
- mdetunilem1
- mdetunilem2
- mdetunilem3
- mdetunilem4
- mdetunilem5
- mdetunilem6
- mdetunilem7
- mdetunilem8
- mdetunilem9
- mdetuni0
- mdetuni
- mdetmul
- Determinants of 2 x 2 -matrices
- m2detleiblem1
- m2detleiblem5
- m2detleiblem6
- m2detleiblem7
- m2detleiblem2
- m2detleiblem3
- m2detleiblem4
- m2detleib
- The matrix adjugate/adjunct
- cmadu
- cminmar1
- df-madu
- df-minmar1
- mndifsplit
- madufval
- maduval
- maducoeval
- maducoeval2
- maduf
- madutpos
- madugsum
- madurid
- madulid
- minmar1fval
- minmar1val0
- minmar1val
- minmar1eval
- minmar1marrep
- minmar1cl
- maducoevalmin1
- Laplace expansion of determinants (special case)
- symgmatr01lem
- symgmatr01
- gsummatr01lem1
- gsummatr01lem2
- gsummatr01lem3
- gsummatr01lem4
- gsummatr01
- marep01ma
- smadiadetlem0
- smadiadetlem1
- smadiadetlem1a
- smadiadetlem2
- smadiadetlem3lem0
- smadiadetlem3lem1
- smadiadetlem3lem2
- smadiadetlem3
- smadiadetlem4
- smadiadet
- smadiadetglem1
- smadiadetglem2
- smadiadetg
- smadiadetg0
- smadiadetr
- Inverse matrix
- invrvald
- matinv
- matunit
- Cramer's rule
- slesolvec
- slesolinv
- slesolinvbi
- slesolex
- cramerimplem1
- cramerimplem2
- cramerimplem3
- cramerimp
- cramerlem1
- cramerlem2
- cramerlem3
- cramer0
- cramer