Metamath Proof Explorer
Table of Contents - 11.7.1. Definition and basic properties
The characteristic polynomial of a matrix is the determinant of the
characteristic matrix of : .
- cchpmat
- df-chpmat
- chmatcl
- chmatval
- chpmatfval
- chpmatval
- chpmatply1
- chpmatval2
- chpmat0d
- chpmat1dlem
- chpmat1d
- chpdmatlem0
- chpdmatlem1
- chpdmatlem2
- chpdmatlem3
- chpdmat
- chpscmat
- chpscmat0
- chpscmatgsumbin
- chpscmatgsummon
- chp0mat
- chpidmat
- chmaidscmat