Integer powers of square matrices #
In this file, we define integer power of matrices, relying on the nonsingular inverse definition for negative powers.
Implementation details #
The main definition is a direct recursive call on the integer inductive type,
as provided by the
DivInvMonoid.Pow default implementation.
The lemma names are taken from
matrix inverse, matrix powers