In automated complexity analysis of term rewriting, estimating the growth rate of the values in A n – for a fixed matrix A and increasing n – is of fundamental interest. This growth rate can be exactly characterized via A’s Jordan normal form (JNF). We formalized this result in our library IsaFoR and our certifier CeTA, and thereby improve the support for certifying polynomial bounds derived by (untrusted) complexity analysis tools. To this end, we develop a new library for matrices that admits to conveniently work with block matrices. Besides the mentioned complexity result, we formalize Gram-Schmidt’s orthogonalization algorithm and Schur decomposition in order to prove existence of JNFs. We also provide a uniqueness result for JNFs which allows us to compute Jordan blocks for individual eigenvalues. In order to determine eigenvalues automatically, we moreover formalize Yun’s square-free factorization algorithm.