Metamath Proof Explorer

Table of Contents - 11.5.2. The characteristic factor function G

In this subsection the function is discussed. This function is involved in the representation of the product of the characteristic matrix of a given matrix and its adjunct as an infinite sum, see cpmadugsum. Therefore, this function is called "characteristic factor function" (in short "chfacf") in the following. It plays an important role in the proof of the Cayley-Hamilton theorem, see cayhamlem1, cayhamlem3 and cayhamlem4.

  1. fvmptnn04if
  2. fvmptnn04ifa
  3. fvmptnn04ifb
  4. fvmptnn04ifc
  5. fvmptnn04ifd
  6. chfacfisf
  7. chfacfisfcpmat
  8. chfacffsupp
  9. chfacfscmulcl
  10. chfacfscmul0
  11. chfacfscmulfsupp
  12. chfacfscmulgsum
  13. chfacfpmmulcl
  14. chfacfpmmul0
  15. chfacfpmmulfsupp
  16. chfacfpmmulgsum
  17. chfacfpmmulgsum2
  18. cayhamlem1