This AFP-entry is mostly marked as legacy, since there is a better
implementation of matrices available in "../Jordan_Normal_Form/Matrix.thy".
That formalization is more abstract, more complete in terms of operations,
and it still provides an efficient implementation.